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  7289  cocan1  7292  curfv  8871  ordiso2  9487  fin1a2lem9  10410  fin1a2lem12  10413  gchpwdom  10679  winainflem  10702  bpolydif  16141  dvdsmodexp  16350  muldvds1  16370  lcmdvds  16698  ramcl  17121  oddvdsnn0  19671  ghmplusg  19973  frlmsslss2  21988  frlmsslsp  22009  islindf4  22051  mamures  22619  matepmcl  22684  matepm2cl  22685  pmatcollpw2lem  23002  cnpnei  23489  ssref  23738  qtopss  23941  elfm2  24174  flffbas  24221  cnpfcf  24267  deg1ldg  26317  brbtwn2  29362  colinearalg  29367  axsegconlem1  29374  upgrpredgv  29596  cusgrrusgr  30041  upgrewlkle2  30066  wwlksm1edg  30349  clwwlkf  30517  wwlksext2clwwlk  30527  nvmul0or  31131  hoadddi  32284  volfiniune  34741  bnj548  35406  funsseq  36347  nn0prpwlem  36941  fnemeet1  36985  lindsadd  38367  keridl  38782  pmapglbx  40642  elpaddn0  40673  paddasslem9  40701  paddasslem10  40702  cdleme42mgN  41361  relexpxpmin  44557  ntrclsk3  44910  n0p  45879  wessf1ornlem  46017  infxr  46196  lptre2pt  46468  dvnprodlem1  46774  fourierdlem42  46977  fourierdlem48  46982  fourierdlem54  46988  fourierdlem77  47011  sge0rpcpnf  47249  hoicvr  47376  smflimsuplem7  47654