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  37799  mblfinlem2  37859  mblfinlem3  37860  mettrifi  37958  ghomdiv  38093  grpokerinj  38094  rngohomco  38175  crngohomfo  38207  keridl  38233  cvrcon3b  39537  mzpsubst  42990  lzunuz  43010  diophrex  43017  rmxycomplete  43159  jm2.26  43244  lnmepi  43327  lmhmlnmsplit  43329  nadd2rabex  43628  nadd1rabtr  43630  nadd1rabex  43632  ntrclsiso  44308  ntrclskb  44310  ntrclsk3  44311  uzwo4  45298  wessf1ornlem  45429  choicefi  45444  supxrgere  45578  supxrgelem  45582  supxrge  45583  suplesup  45584  infxr  45611  infleinflem2  45615  rexabslelem  45662  fmul01lt1  45832  limcleqr  45888  limclner  45895  dvnprodlem1  46190  volioc  46216  stoweidlem60  46304  wallispilem3  46311  fourierdlem12  46363  fourierdlem41  46392  fourierdlem42  46393  fourierdlem48  46398  fourierdlem49  46399  fourierdlem54  46404  fourierdlem68  46418  fourierdlem73  46423  fourierdlem74  46424  fourierdlem75  46425  fourierdlem83  46433  elaa2  46478  etransclem24  46502  etransclem32  46510  ioorrnopnlem  46548  issalnnd  46589  sge0xaddlem2  46678  sge0seq  46690  meaiininc2  46732  hoicvr  46792  ovnsubaddlem2  46815  hoidmvval0  46831  hoidmvlelem3  46841  hspmbllem2  46871  vonioo  46926  vonicc  46929  smfinflem  47061  fsupdm  47086  finfdm  47090  fmtnoprmfac2lem1  47812  fmtnofac1  47816  lincresunit3lem3  48720  suppdm  48756  inlinecirc02p  49033