Theorem 3adant3r 1323

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)

Hypothesis

Ref	Expression
3adant1l.1	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
3adant3r	|- ( ( ph /\ ps /\ ( ch /\ ta ) ) -> th )

Proof of Theorem 3adant3r

Step	Hyp	Ref	Expression
1		3adant1l.1	. . . 4 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3com13 1270	. . 3 |- ( ( ch /\ ps /\ ph ) -> th )
3	2	3adant1r 1319	. 2 |- ( ( ( ch /\ ta ) /\ ps /\ ph ) -> th )
4	3	3com13 1270	1 |- ( ( ph /\ ps /\ ( ch /\ ta ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  wfrlem12  7426  mapfien2  8314  cfeq0  9078  ltmul2  10874  lemul1  10875  lemul2  10876  lemuldiv  10903  lediv2  10913  ltdiv23  10914  lediv23  10915  dvdscmulr  15010  dvdsmulcr  15011  modremain  15132  ndvdsadd  15134  rpexp12i  15434  isdrngd  18772  cramerimp  20492  tsmsxp  21958  xblcntrps  22215  xblcntr  22216  rrxmet  23191  nvaddsub4  27512  hvmulcan2  27930  adjlnop  28945  frrlem11  31792  rrnmet  33628  lfladd  34353  lflsub  34354  lshpset2N  34406  atcvrj1  34717  athgt  34742  ltrncnvel  35428  trlcnv  35452  trljat2  35454  cdlemc5  35482  trlcoabs  36009  trlcolem  36014  dicvaddcl  36479  limsupre3uzlem  39967  fourierdlem42  40366  ovnhoilem2  40816  lincext3  42245