Theorem 3ad2antl2 1186

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 1166	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  1192  simpl2l  1226  simpl2r  1227  simpl21  1251  simpl22  1252  simpl23  1253  fcofo  7309  cocan1  7312  ordiso2  9556  fin1a2lem9  10449  fin1a2lem12  10452  gchpwdom  10711  winainflem  10734  bpolydif  16092  dvdsmodexp  16299  muldvds1  16319  lcmdvds  16646  ramcl  17068  oddvdsnn0  19563  ghmplusg  19865  frlmsslss2  21796  frlmsslsp  21817  islindf4  21859  mamures  22402  matepmcl  22469  matepm2cl  22470  pmatcollpw2lem  22784  cnpnei  23273  ssref  23521  qtopss  23724  elfm2  23957  flffbas  24004  cnpfcf  24050  deg1ldg  26132  brbtwn2  28921  colinearalg  28926  axsegconlem1  28933  upgrpredgv  29157  cusgrrusgr  29600  upgrewlkle2  29625  wwlksm1edg  29902  clwwlkf  30067  wwlksext2clwwlk  30077  nvmul0or  30670  hoadddi  31823  volfiniune  34232  bnj548  34912  funsseq  35769  nn0prpwlem  36324  fnemeet1  36368  curfv  37608  lindsadd  37621  keridl  38040  pmapglbx  39772  elpaddn0  39803  paddasslem9  39831  paddasslem10  39832  cdleme42mgN  40491  factwoffsmonot  42244  relexpxpmin  43735  ntrclsk3  44088  n0p  45055  wessf1ornlem  45195  infxr  45383  lptre2pt  45660  dvnprodlem1  45966  fourierdlem42  46169  fourierdlem48  46174  fourierdlem54  46180  fourierdlem77  46203  sge0rpcpnf  46441  hoicvr  46568  smflimsuplem7  46846