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  7234  cocan1  7237  ordiso2  9420  fin1a2lem9  10318  fin1a2lem12  10321  gchpwdom  10581  winainflem  10604  bpolydif  15978  dvdsmodexp  16187  muldvds1  16207  lcmdvds  16535  ramcl  16957  oddvdsnn0  19473  ghmplusg  19775  frlmsslss2  21730  frlmsslsp  21751  islindf4  21793  mamures  22341  matepmcl  22406  matepm2cl  22407  pmatcollpw2lem  22721  cnpnei  23208  ssref  23456  qtopss  23659  elfm2  23892  flffbas  23939  cnpfcf  23985  deg1ldg  26053  brbtwn2  28978  colinearalg  28983  axsegconlem1  28990  upgrpredgv  29212  cusgrrusgr  29655  upgrewlkle2  29680  wwlksm1edg  29954  clwwlkf  30122  wwlksext2clwwlk  30132  nvmul0or  30725  hoadddi  31878  volfiniune  34387  bnj548  35053  funsseq  35962  nn0prpwlem  36516  fnemeet1  36560  curfv  37801  lindsadd  37814  keridl  38233  pmapglbx  40029  elpaddn0  40060  paddasslem9  40088  paddasslem10  40089  cdleme42mgN  40748  relexpxpmin  43958  ntrclsk3  44311  n0p  45290  wessf1ornlem  45429  infxr  45611  lptre2pt  45884  dvnprodlem1  46190  fourierdlem42  46393  fourierdlem48  46398  fourierdlem54  46404  fourierdlem77  46427  sge0rpcpnf  46665  hoicvr  46792  smflimsuplem7  47070