Theorem 3ad2antl2 1205

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 728	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)
3	2	3adantl1 1185	1 ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpl2  1211  simpl2l  1245  simpl2r  1246  simpl21  1270  simpl22  1271  simpl23  1272  fcofo  7295  cocan1  7298  ordiso2  9484  fin1a2lem9  10407  fin1a2lem12  10410  gchpwdom  10670  winainflem  10693  bpolydif  16131  dvdsmodexp  16340  muldvds1  16360  lcmdvds  16688  ramcl  17111  oddvdsnn0  19658  ghmplusg  19960  frlmsslss2  21975  frlmsslsp  21996  islindf4  22038  mamures  22604  matepmcl  22669  matepm2cl  22670  pmatcollpw2lem  22984  cnpnei  23471  ssref  23720  qtopss  23923  elfm2  24156  flffbas  24203  cnpfcf  24249  deg1ldg  26300  brbtwn2  29310  colinearalg  29315  axsegconlem1  29322  upgrpredgv  29544  cusgrrusgr  29989  upgrewlkle2  30014  wwlksm1edg  30297  clwwlkf  30465  wwlksext2clwwlk  30475  nvmul0or  31073  hoadddi  32226  volfiniune  34685  bnj548  35350  funsseq  36297  nn0prpwlem  36890  fnemeet1  36934  curfv  38308  lindsadd  38321  keridl  38741  pmapglbx  40601  elpaddn0  40632  paddasslem9  40660  paddasslem10  40661  cdleme42mgN  41320  relexpxpmin  44501  ntrclsk3  44854  n0p  45823  wessf1ornlem  45961  infxr  46140  lptre2pt  46412  dvnprodlem1  46718  fourierdlem42  46921  fourierdlem48  46926  fourierdlem54  46932  fourierdlem77  46955  sge0rpcpnf  47193  hoicvr  47320  smflimsuplem7  47598