Theorem 3ad2antl2 1187

Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)

Hypothesis

Ref	Expression
3ad2antl.1	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3ad2antl2	⊢ (((𝜓 ∧ 𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Proof of Theorem 3ad2antl2

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
2	1	adantlr 715	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)
3	2	3adantl1 1167	1 ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simpl2  1193  simpl2l  1227  simpl2r  1228  simpl21  1252  simpl22  1253  simpl23  1254  fcofo  7232  cocan1  7235  ordiso2  9418  fin1a2lem9  10316  fin1a2lem12  10319  gchpwdom  10579  winainflem  10602  bpolydif  15976  dvdsmodexp  16185  muldvds1  16205  lcmdvds  16533  ramcl  16955  oddvdsnn0  19471  ghmplusg  19773  frlmsslss2  21728  frlmsslsp  21749  islindf4  21791  mamures  22339  matepmcl  22404  matepm2cl  22405  pmatcollpw2lem  22719  cnpnei  23206  ssref  23454  qtopss  23657  elfm2  23890  flffbas  23937  cnpfcf  23983  deg1ldg  26051  brbtwn2  28927  colinearalg  28932  axsegconlem1  28939  upgrpredgv  29161  cusgrrusgr  29604  upgrewlkle2  29629  wwlksm1edg  29903  clwwlkf  30071  wwlksext2clwwlk  30081  nvmul0or  30674  hoadddi  31827  volfiniune  34336  bnj548  35002  funsseq  35911  nn0prpwlem  36465  fnemeet1  36509  curfv  37740  lindsadd  37753  keridl  38172  pmapglbx  39968  elpaddn0  39999  paddasslem9  40027  paddasslem10  40028  cdleme42mgN  40687  relexpxpmin  43900  ntrclsk3  44253  n0p  45232  wessf1ornlem  45371  infxr  45553  lptre2pt  45826  dvnprodlem1  46132  fourierdlem42  46335  fourierdlem48  46340  fourierdlem54  46346  fourierdlem77  46369  sge0rpcpnf  46607  hoicvr  46734  smflimsuplem7  47012