Theorem 3ad2antl1 1199

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 725	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)
3	2	3adantl2 1181	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

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

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 209  df-an 400  df-3an 1100

This theorem is referenced by:  simpl1  1205  simpl1l  1238  simpl1r  1239  simpl11  1262  simpl12  1263  simpl13  1264  smocdmdom  8339  omeulem1  8551  f1oen4g  8945  f1dom4g  8946  dif1ennnALT  9221  ordiso2  9463  infpssrlem4  10263  fin1a2lem9  10365  gchpwdom  10628  tskwun  10742  gruxp  10765  infregelb  12176  fzo1fzo0n0  13721  fsuppmapnn0fiub  14004  pfxsuffeqwrdeq  14711  fprodle  16026  muldvds2  16315  dvds2add  16324  dvds2sub  16325  dvdstr  16328  lcmfledvds  16666  mndvcl  18831  mhmvlin  18835  mulgnnsubcl  19128  mulgpropd  19158  gexdvdsi  19623  ringidss  20327  reslmhm2  21120  obs2ss  21781  lsslindf  21882  issubassa  21919  madurid  22704  restntr  23242  cnpnei  23324  upxp  23683  qtopss  23775  opnfbas  23902  fbasrn  23944  trfg  23951  ufilmax  23967  ustuqtop1  24301  prdsxmetlem  24428  nmoix  24789  nmoi2  24790  iimulcl  24999  mbfimaopn2  25719  lgsval4lem  27372  nodenselem8  27755  f1otrg  29071  brbtwn2  29106  colinearalg  29111  axsegconlem1  29118  0vtxrusgr  29778  clwwlkccatlem  30191  clwwlkccat  30192  clwwisshclwws  30217  clwwlkfo  30252  numclwwlk1lem2fo  30560  lnosub  30962  pjspansn  31780  eulerpartlemb  34665  cnpconn  35580  mclspps  35934  curf  38097  mblfinlem2  38157  mblfinlem3  38158  mettrifi  38256  ghomdiv  38391  grpokerinj  38392  rngohomco  38473  crngohomfo  38505  keridl  38531  cvrcon3b  39901  mzpsubst  43329  lzunuz  43349  diophrex  43356  rmxycomplete  43494  jm2.26  43579  lnmepi  43662  lmhmlnmsplit  43664  nadd2rabex  43963  nadd1rabtr  43965  nadd1rabex  43967  ntrclsiso  44643  ntrclskb  44645  ntrclsk3  44646  uzwo4  45633  wessf1ornlem  45763  choicefi  45777  supxrgere  45909  supxrgelem  45913  supxrge  45914  suplesup  45915  infxr  45942  infleinflem2  45946  rexabslelem  45992  fmul01lt1  46162  limcleqr  46218  limclner  46225  dvnprodlem1  46520  volioc  46546  stoweidlem60  46634  wallispilem3  46641  fourierdlem12  46693  fourierdlem41  46722  fourierdlem42  46723  fourierdlem48  46728  fourierdlem49  46729  fourierdlem54  46734  fourierdlem68  46748  fourierdlem73  46753  fourierdlem74  46754  fourierdlem75  46755  fourierdlem83  46763  elaa2  46808  etransclem24  46832  etransclem32  46840  ioorrnopnlem  46878  issalnnd  46919  sge0xaddlem2  47008  sge0seq  47020  meaiininc2  47062  hoicvr  47122  ovnsubaddlem2  47145  hoidmvval0  47161  hoidmvlelem3  47171  hspmbllem2  47201  vonioo  47256  vonicc  47259  smfinflem  47391  fsupdm  47416  finfdm  47420  fmtnoprmfac2lem1  48175  fmtnofac1  48179  lincresunit3lem3  49096  suppdm  49132  inlinecirc02p  49409