Theorem 3ad2antl2 1183

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

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

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  simpl2  1189  simpl2l  1223  simpl2r  1224  simpl21  1248  simpl22  1249  simpl23  1250  fcofo  7022  cocan1  7025  ordiso2  8963  fin1a2lem9  9819  fin1a2lem12  9822  gchpwdom  10081  winainflem  10104  bpolydif  15401  dvdsmodexp  15607  muldvds1  15626  lcmdvds  15942  ramcl  16355  gsumccatOLD  17997  oddvdsnn0  18664  ghmplusg  18959  frlmsslss2  20464  frlmsslsp  20485  islindf4  20527  mamures  20997  matepmcl  21067  matepm2cl  21068  pmatcollpw2lem  21382  cnpnei  21869  ssref  22117  qtopss  22320  elfm2  22553  flffbas  22600  cnpfcf  22646  deg1ldg  24693  brbtwn2  26699  colinearalg  26704  axsegconlem1  26711  upgrpredgv  26932  cusgrrusgr  27371  upgrewlkle2  27396  wwlksm1edg  27667  clwwlkf  27832  wwlksext2clwwlk  27842  nvmul0or  28433  hoadddi  29586  volfiniune  31599  bnj548  32279  funsseq  33124  nn0prpwlem  33783  fnemeet1  33827  curfv  35037  lindsadd  35050  keridl  35470  pmapglbx  37065  elpaddn0  37096  paddasslem9  37124  paddasslem10  37125  cdleme42mgN  37784  factwoffsmonot  39388  relexpxpmin  40418  ntrclsk3  40773  n0p  41677  wessf1ornlem  41811  infxr  41999  lptre2pt  42282  dvnprodlem1  42588  fourierdlem42  42791  fourierdlem48  42796  fourierdlem54  42802  fourierdlem77  42825  sge0rpcpnf  43060  hoicvr  43187  smflimsuplem7  43457  isomgrsym  44354