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  7294  cocan1  7297  onelfvnef1  8442  curfv  8885  ordiso2  9502  fin1a2lem9  10479  fin1a2lem12  10482  gchpwdom  10748  winainflem  10771  bpolydif  16214  dvdsmodexp  16423  muldvds1  16443  lcmdvds  16776  ramcl  17200  oddvdsnn0  19751  ghmplusg  20053  frlmsslss2  22074  frlmsslsp  22095  islindf4  22137  mamures  22705  matepmcl  22770  matepm2cl  22771  pmatcollpw2lem  23088  cnpnei  23575  ssref  23824  qtopss  24027  elfm2  24260  flffbas  24307  cnpfcf  24353  deg1ldg  26403  brbtwn2  29476  colinearalg  29481  axsegconlem1  29488  upgrpredgv  29710  cusgrrusgr  30155  upgrewlkle2  30180  wwlksm1edg  30463  clwwlkf  30631  wwlksext2clwwlk  30641  nvmul0or  31245  hoadddi  32398  volfiniune  34856  bnj548  35520  funsseq  36512  nn0prpwlem  37090  fnemeet1  37134  lindsadd  38516  keridl  38946  pmapglbx  40806  elpaddn0  40837  paddasslem9  40865  paddasslem10  40866  cdleme42mgN  41525  relexpxpmin  44702  ntrclsk3  45055  n0p  46031  wessf1ornlem  46169  infxr  46347  lptre2pt  46619  dvnprodlem1  46925  fourierdlem42  47128  fourierdlem48  47133  fourierdlem54  47139  fourierdlem77  47162  sge0rpcpnf  47400  hoicvr  47527  smflimsuplem7  47805