MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3adantl3 Structured version   Visualization version   GIF version

Theorem 3adantl3 1169
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
Hypothesis
Ref Expression
3adantl.1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
3adantl3 (((𝜑𝜓𝜏) ∧ 𝜒) → 𝜃)

Proof of Theorem 3adantl3
StepHypRef Expression
1 3simpa 1149 . 2 ((𝜑𝜓𝜏) → (𝜑𝜓))
2 3adantl.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 581 1 (((𝜑𝜓𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  dif1ennnALT  9227  infpssrlem4  10250  fin23lem11  10261  tskwun  10728  gruf  10755  lediv2a  12057  prunioo  13407  nn0p1elfzo  13624  hashunsnggt  14303  rpnnen2lem7  16110  muldvds1  16171  muldvds2  16172  dvdscmul  16173  dvdsmulc  16174  rpexp  16606  pospropd  18224  mdetmul  21995  elcls  22447  iscnp4  22637  cnpnei  22638  cnpflf2  23374  cnpflf  23375  cnpfcf  23415  xbln0  23790  blcls  23885  iimulcl  24323  icccvx  24336  iscau2  24664  rrxcph  24779  cncombf  25045  mumul  26553  noetalem1  27112  ax5seglem1  27926  ax5seglem2  27927  wwlksnext  28887  clwwlkinwwlk  29033  nvmul0or  29641  fh1  30609  fh2  30610  cm2j  30611  pjoi0  30708  hoadddi  30794  hmopco  31014  padct  31690  iocinif  31738  volfiniune  32893  eulerpartlemb  33032  ivthALT  34860  lindsadd  36121  cnambfre  36176  rngohomco  36483  rngoisoco  36491  pexmidlem3N  38485  hdmapglem7  40442  sticksstones12a  40615  factwoffsmonot  40665  relexpmulg  42074  supxrgere  43658  supxrgelem  43662  supxrge  43663  infxr  43692  infleinflem2  43696  rexabslelem  43743  pimxrneun  43814  lptre2pt  43971  fnlimfvre  44005  limsupmnfuzlem  44057  climisp  44077  limsupgtlem  44108  dvnprodlem1  44277  ibliccsinexp  44282  iblioosinexp  44284  fourierdlem12  44450  fourierdlem41  44479  fourierdlem42  44480  fourierdlem48  44485  fourierdlem49  44486  fourierdlem51  44488  fourierdlem73  44510  fourierdlem74  44511  fourierdlem75  44512  fourierdlem97  44534  etransclem24  44589  ioorrnopnlem  44635  issalnnd  44676  sge0rpcpnf  44752  sge0seq  44777  meaiuninc3v  44815  smfmullem4  45125  smflimsupmpt  45160  smfliminfmpt  45163  lincdifsn  46595
  Copyright terms: Public domain W3C validator