Theorem 3ad2antl2 1199

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  simpl2  1205  simpl2l  1239  simpl2r  1240  simpl21  1264  simpl22  1265  simpl23  1266  fcofo  7267  cocan1  7270  ordiso2  9457  fin1a2lem9  10359  fin1a2lem12  10362  gchpwdom  10622  winainflem  10645  bpolydif  16076  dvdsmodexp  16285  muldvds1  16305  lcmdvds  16633  ramcl  17056  oddvdsnn0  19575  ghmplusg  19877  frlmsslss2  21815  frlmsslsp  21836  islindf4  21878  mamures  22445  matepmcl  22510  matepm2cl  22511  pmatcollpw2lem  22825  cnpnei  23312  ssref  23560  qtopss  23763  elfm2  23996  flffbas  24043  cnpfcf  24089  deg1ldg  26140  brbtwn2  29063  colinearalg  29068  axsegconlem1  29075  upgrpredgv  29297  cusgrrusgr  29739  upgrewlkle2  29764  wwlksm1edg  30038  clwwlkf  30206  wwlksext2clwwlk  30216  nvmul0or  30810  hoadddi  31963  volfiniune  34488  bnj548  35153  funsseq  36079  nn0prpwlem  36643  fnemeet1  36687  curfv  38060  lindsadd  38073  keridl  38492  pmapglbx  40354  elpaddn0  40385  paddasslem9  40413  paddasslem10  40414  cdleme42mgN  41073  relexpxpmin  44254  ntrclsk3  44607  n0p  45586  wessf1ornlem  45724  infxr  45903  lptre2pt  46175  dvnprodlem1  46481  fourierdlem42  46684  fourierdlem48  46689  fourierdlem54  46695  fourierdlem77  46718  sge0rpcpnf  46956  hoicvr  47083  smflimsuplem7  47361