Theorem 3ad2antl1 1204

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpl1  1210  simpl1l  1243  simpl1r  1244  simpl11  1267  simpl12  1268  simpl13  1269  smocdmdom  8414  omeulem1  8628  curf  8928  f1oen4g  9029  f1dom4g  9030  dif1ennnALT  9306  ordiso2  9546  infpssrlem4  10423  fin1a2lem9  10525  gchpwdom  10794  tskwun  10908  gruxp  10931  infregelb  12341  fzo1fzo0n0  13890  fsuppmapnn0fiub  14174  pfxsuffeqwrdeq  14889  fprodle  16207  muldvds2  16495  dvds2add  16504  dvds2sub  16505  dvdstr  16508  lcmfledvds  16851  mndvcl  19042  mhmvlin  19046  mulgnnsubcl  19346  mulgpropd  19376  gexdvdsi  19848  ringidss  20557  reslmhm2  21379  obs2ss  22090  lsslindf  22191  issubassa  22230  madurid  23014  restntr  23555  cnpnei  23637  upxp  23997  qtopss  24089  opnfbas  24216  fbasrn  24258  trfg  24265  ufilmax  24281  ustuqtop1  24615  prdsxmetlem  24742  nmoix  25103  nmoi2  25104  iimulcl  25313  mbfimaopn2  26033  lgsval4lem  27692  nodenselem8  28105  f1otrg  29505  brbtwn2  29540  colinearalg  29545  axsegconlem1  29552  0vtxrusgr  30215  clwwlkccatlem  30637  clwwlkccat  30638  clwwisshclwws  30663  clwwlkfo  30698  numclwwlk1lem2fo  31016  lnosub  31418  pjspansn  32236  eulerpartlemb  35111  cnpconn  36203  mclspps  36557  mblfinlem2  38844  mblfinlem3  38845  mettrifi  38957  ghomdiv  39092  grpokerinj  39093  rngohomco  39174  crngohomfo  39206  keridl  39232  cvrcon3b  40600  mzpsubst  44025  lzunuz  44045  diophrex  44052  rmxycomplete  44190  jm2.26  44275  lnmepi  44353  lmhmlnmsplit  44355  nadd2rabex  44649  nadd1rabtr  44651  nadd1rabex  44653  ntrclsiso  45328  ntrclskb  45330  ntrclsk3  45331  uzwo4  46344  wessf1ornlem  46473  choicefi  46487  supxrgere  46618  supxrgelem  46622  supxrge  46623  suplesup  46624  infxr  46651  infleinflem2  46655  rexabslelem  46701  fmul01lt1  46871  limcleqr  46927  limclner  46934  dvnprodlem1  47229  volioc  47255  stoweidlem60  47343  wallispilem3  47350  fourierdlem12  47402  fourierdlem41  47431  fourierdlem42  47432  fourierdlem48  47437  fourierdlem49  47438  fourierdlem54  47443  fourierdlem68  47457  fourierdlem73  47462  fourierdlem74  47463  fourierdlem75  47464  fourierdlem83  47472  elaa2  47517  etransclem24  47541  etransclem32  47549  ioorrnopnlem  47587  issalnnd  47628  sge0xaddlem2  47717  sge0seq  47729  meaiininc2  47771  hoicvr  47831  ovnsubaddlem2  47854  hoidmvval0  47870  hoidmvlelem3  47880  hspmbllem2  47910  vonioo  47965  vonicc  47968  smfinflem  48100  fsupdm  48125  finfdm  48129  fmtnoprmfac2lem1  48924  fmtnofac1  48928  lincresunit3lem3  49917  suppdm  49953  inlinecirc02p  50230