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  7225  cocan1  7228  ordiso2  9407  fin1a2lem9  10302  fin1a2lem12  10305  gchpwdom  10564  winainflem  10587  bpolydif  15962  dvdsmodexp  16171  muldvds1  16191  lcmdvds  16519  ramcl  16941  oddvdsnn0  19423  ghmplusg  19725  frlmsslss2  21682  frlmsslsp  21703  islindf4  21745  mamures  22282  matepmcl  22347  matepm2cl  22348  pmatcollpw2lem  22662  cnpnei  23149  ssref  23397  qtopss  23600  elfm2  23833  flffbas  23880  cnpfcf  23926  deg1ldg  25995  brbtwn2  28850  colinearalg  28855  axsegconlem1  28862  upgrpredgv  29084  cusgrrusgr  29527  upgrewlkle2  29552  wwlksm1edg  29826  clwwlkf  29991  wwlksext2clwwlk  30001  nvmul0or  30594  hoadddi  31747  volfiniune  34197  bnj548  34864  funsseq  35741  nn0prpwlem  36296  fnemeet1  36340  curfv  37580  lindsadd  37593  keridl  38012  pmapglbx  39748  elpaddn0  39779  paddasslem9  39807  paddasslem10  39808  cdleme42mgN  40467  relexpxpmin  43690  ntrclsk3  44043  n0p  45023  wessf1ornlem  45163  infxr  45346  lptre2pt  45621  dvnprodlem1  45927  fourierdlem42  46130  fourierdlem48  46135  fourierdlem54  46141  fourierdlem77  46164  sge0rpcpnf  46402  hoicvr  46529  smflimsuplem7  46807