Theorem 3ad2antl2 1182

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  simpl2  1188  simpl2l  1222  simpl2r  1223  simpl21  1247  simpl22  1248  simpl23  1249  fcofo  7046  cocan1  7049  ordiso2  8981  fin1a2lem9  9832  fin1a2lem12  9835  gchpwdom  10094  winainflem  10117  bpolydif  15411  dvdsmodexp  15617  muldvds1  15636  lcmdvds  15954  ramcl  16367  gsumccatOLD  18007  oddvdsnn0  18674  ghmplusg  18968  frlmsslss2  20921  frlmsslsp  20942  islindf4  20984  mamures  21003  matepmcl  21073  matepm2cl  21074  pmatcollpw2lem  21387  cnpnei  21874  ssref  22122  qtopss  22325  elfm2  22558  flffbas  22605  cnpfcf  22651  deg1ldg  24688  brbtwn2  26693  colinearalg  26698  axsegconlem1  26705  upgrpredgv  26926  cusgrrusgr  27365  upgrewlkle2  27390  wwlksm1edg  27661  clwwlkf  27828  wwlksext2clwwlk  27838  nvmul0or  28429  hoadddi  29582  volfiniune  31491  bnj548  32171  funsseq  33013  nn0prpwlem  33672  fnemeet1  33716  curfv  34874  lindsadd  34887  keridl  35312  pmapglbx  36907  elpaddn0  36938  paddasslem9  36966  paddasslem10  36967  cdleme42mgN  37626  factwoffsmonot  39105  relexpxpmin  40069  ntrclsk3  40427  n0p  41312  wessf1ornlem  41452  infxr  41642  lptre2pt  41928  dvnprodlem1  42238  fourierdlem42  42441  fourierdlem48  42446  fourierdlem54  42452  fourierdlem77  42475  sge0rpcpnf  42710  hoicvr  42837  smflimsuplem7  43107  isomgrsym  44008