Theorem 3ad2antl2 1185

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simpl2  1191  simpl2l  1225  simpl2r  1226  simpl21  1250  simpl22  1251  simpl23  1252  fcofo  7169  cocan1  7172  ordiso2  9283  fin1a2lem9  10173  fin1a2lem12  10176  gchpwdom  10435  winainflem  10458  bpolydif  15774  dvdsmodexp  15980  muldvds1  15999  lcmdvds  16322  ramcl  16739  gsumccatOLD  18488  oddvdsnn0  19161  ghmplusg  19456  frlmsslss2  20991  frlmsslsp  21012  islindf4  21054  mamures  21548  matepmcl  21620  matepm2cl  21621  pmatcollpw2lem  21935  cnpnei  22424  ssref  22672  qtopss  22875  elfm2  23108  flffbas  23155  cnpfcf  23201  deg1ldg  25266  brbtwn2  27282  colinearalg  27287  axsegconlem1  27294  upgrpredgv  27518  cusgrrusgr  27957  upgrewlkle2  27982  wwlksm1edg  28255  clwwlkf  28420  wwlksext2clwwlk  28430  nvmul0or  29021  hoadddi  30174  volfiniune  32207  bnj548  32886  funsseq  33751  nn0prpwlem  34520  fnemeet1  34564  curfv  35766  lindsadd  35779  keridl  36199  pmapglbx  37790  elpaddn0  37821  paddasslem9  37849  paddasslem10  37850  cdleme42mgN  38509  factwoffsmonot  40170  relexpxpmin  41332  ntrclsk3  41687  n0p  42598  wessf1ornlem  42729  infxr  42913  lptre2pt  43188  dvnprodlem1  43494  fourierdlem42  43697  fourierdlem48  43702  fourierdlem54  43708  fourierdlem77  43731  sge0rpcpnf  43966  hoicvr  44093  smflimsuplem7  44370  isomgrsym  45299