Theorem 3ad2antl1 1186

Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)

Hypothesis

Ref	Expression
3ad2antl.1	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3ad2antl1	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Proof of Theorem 3ad2antl1

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
2	1	adantlr 715	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)
3	2	3adantl2 1168	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:  simpl1  1192  simpl1l  1225  simpl1r  1226  simpl11  1249  simpl12  1250  simpl13  1251  smocdmdom  8300  omeulem1  8509  f1oen4g  8901  f1dom4g  8902  dif1ennnALT  9177  ordiso2  9420  infpssrlem4  10216  fin1a2lem9  10318  gchpwdom  10581  tskwun  10695  gruxp  10718  infregelb  12126  fzo1fzo0n0  13631  fsuppmapnn0fiub  13914  pfxsuffeqwrdeq  14621  fprodle  15919  muldvds2  16208  dvds2add  16217  dvds2sub  16218  dvdstr  16221  lcmfledvds  16559  mndvcl  18722  mhmvlin  18726  mulgnnsubcl  19016  mulgpropd  19046  gexdvdsi  19512  ringidss  20212  reslmhm2  21005  obs2ss  21684  lsslindf  21785  issubassa  21822  madurid  22588  restntr  23126  cnpnei  23208  upxp  23567  qtopss  23659  opnfbas  23786  fbasrn  23828  trfg  23835  ufilmax  23851  ustuqtop1  24185  prdsxmetlem  24312  nmoix  24673  nmoi2  24674  iimulcl  24889  mbfimaopn2  25614  lgsval4lem  27275  nodenselem8  27659  f1otrg  28943  brbtwn2  28978  colinearalg  28983  axsegconlem1  28990  0vtxrusgr  29651  clwwlkccatlem  30064  clwwlkccat  30065  clwwisshclwws  30090  clwwlkfo  30125  numclwwlk1lem2fo  30433  lnosub  30834  pjspansn  31652  eulerpartlemb  34525  cnpconn  35424  mclspps  35778  curf  37795  mblfinlem2  37855  mblfinlem3  37856  mettrifi  37954  ghomdiv  38089  grpokerinj  38090  rngohomco  38171  crngohomfo  38203  keridl  38229  cvrcon3b  39533  mzpsubst  42986  lzunuz  43006  diophrex  43013  rmxycomplete  43155  jm2.26  43240  lnmepi  43323  lmhmlnmsplit  43325  nadd2rabex  43624  nadd1rabtr  43626  nadd1rabex  43628  ntrclsiso  44304  ntrclskb  44306  ntrclsk3  44307  uzwo4  45294  wessf1ornlem  45425  choicefi  45440  supxrgere  45574  supxrgelem  45578  supxrge  45579  suplesup  45580  infxr  45607  infleinflem2  45611  rexabslelem  45658  fmul01lt1  45828  limcleqr  45884  limclner  45891  dvnprodlem1  46186  volioc  46212  stoweidlem60  46300  wallispilem3  46307  fourierdlem12  46359  fourierdlem41  46388  fourierdlem42  46389  fourierdlem48  46394  fourierdlem49  46395  fourierdlem54  46400  fourierdlem68  46414  fourierdlem73  46419  fourierdlem74  46420  fourierdlem75  46421  fourierdlem83  46429  elaa2  46474  etransclem24  46498  etransclem32  46506  ioorrnopnlem  46544  issalnnd  46585  sge0xaddlem2  46674  sge0seq  46686  meaiininc2  46728  hoicvr  46788  ovnsubaddlem2  46811  hoidmvval0  46827  hoidmvlelem3  46837  hspmbllem2  46867  vonioo  46922  vonicc  46925  smfinflem  47057  fsupdm  47082  finfdm  47086  fmtnoprmfac2lem1  47808  fmtnofac1  47812  lincresunit3lem3  48716  suppdm  48752  inlinecirc02p  49029