Theorem 3ad2antl2 1184

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  simpl2  1190  simpl2l  1224  simpl2r  1225  simpl21  1249  simpl22  1250  simpl23  1251  fcofo  7140  cocan1  7143  ordiso2  9204  fin1a2lem9  10095  fin1a2lem12  10098  gchpwdom  10357  winainflem  10380  bpolydif  15693  dvdsmodexp  15899  muldvds1  15918  lcmdvds  16241  ramcl  16658  gsumccatOLD  18394  oddvdsnn0  19067  ghmplusg  19362  frlmsslss2  20892  frlmsslsp  20913  islindf4  20955  mamures  21449  matepmcl  21519  matepm2cl  21520  pmatcollpw2lem  21834  cnpnei  22323  ssref  22571  qtopss  22774  elfm2  23007  flffbas  23054  cnpfcf  23100  deg1ldg  25162  brbtwn2  27176  colinearalg  27181  axsegconlem1  27188  upgrpredgv  27412  cusgrrusgr  27851  upgrewlkle2  27876  wwlksm1edg  28147  clwwlkf  28312  wwlksext2clwwlk  28322  nvmul0or  28913  hoadddi  30066  volfiniune  32098  bnj548  32777  funsseq  33648  nn0prpwlem  34438  fnemeet1  34482  curfv  35684  lindsadd  35697  keridl  36117  pmapglbx  37710  elpaddn0  37741  paddasslem9  37769  paddasslem10  37770  cdleme42mgN  38429  factwoffsmonot  40091  relexpxpmin  41214  ntrclsk3  41569  n0p  42480  wessf1ornlem  42611  infxr  42796  lptre2pt  43071  dvnprodlem1  43377  fourierdlem42  43580  fourierdlem48  43585  fourierdlem54  43591  fourierdlem77  43614  sge0rpcpnf  43849  hoicvr  43976  smflimsuplem7  44246  isomgrsym  45176