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

Theorem 3adantl3 1174
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 1143 . 2 ((𝜑𝜓𝜏) → (𝜑𝜓))
2 3adantl.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 489 1 (((𝜑𝜓𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  dif1en  8360  infpssrlem4  9340  fin23lem11  9351  tskwun  9818  gruf  9845  lediv2a  11129  prunioo  12514  nn0p1elfzo  12725  rpnnen2lem7  15168  muldvds1  15228  muldvds2  15229  dvdscmul  15230  dvdsmulc  15231  rpexp  15654  pospropd  17355  mdetmul  20651  elcls  21099  iscnp4  21289  cnpnei  21290  cnpflf2  22025  cnpflf  22026  cnpfcf  22066  xbln0  22440  blcls  22532  iimulcl  22957  icccvx  22970  iscau2  23295  rrxcph  23400  cncombf  23644  mumul  25127  ax5seglem1  26028  ax5seglem2  26029  clwwlkinwwlk  27190  wwlksext2clwwlkOLD  27209  nvmul0or  27835  fh1  28807  fh2  28808  cm2j  28809  pjoi0  28906  hoadddi  28992  hmopco  29212  padct  29827  iocinif  29873  volfiniune  30623  eulerpartlemb  30760  ivthALT  32657  cnambfre  33789  rngohomco  34104  rngoisoco  34112  pexmidlem3N  35779  hdmapglem7  37741  relexpmulg  38522  supxrgere  40065  supxrgelem  40069  supxrge  40070  infxr  40099  infleinflem2  40103  rexabslelem  40161  lptre2pt  40393  fnlimfvre  40427  limsupmnfuzlem  40479  climisp  40499  limsupgtlem  40530  dvnprodlem1  40682  ibliccsinexp  40687  iblioosinexp  40689  fourierdlem12  40857  fourierdlem41  40886  fourierdlem42  40887  fourierdlem48  40892  fourierdlem49  40893  fourierdlem51  40895  fourierdlem73  40917  fourierdlem74  40918  fourierdlem75  40919  fourierdlem97  40941  etransclem24  40996  ioorrnopnlem  41045  issalnnd  41084  sge0rpcpnf  41159  sge0seq  41184  meaiuninc3v  41222  smfmullem4  41525  smflimsupmpt  41559  smfliminfmpt  41562  lincdifsn  42741
  Copyright terms: Public domain W3C validator