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

Theorem 3adantl3 1239
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 1078 . 2 ((𝜑𝜓𝜏) → (𝜑𝜓))
2 3adantl.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 487 1 (((𝜑𝜓𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 1056
This theorem is referenced by:  dif1en  8234  infpssrlem4  9166  fin23lem11  9177  tskwun  9644  gruf  9671  lediv2a  10955  prunioo  12339  nn0p1elfzo  12550  rpnnen2lem7  14993  muldvds1  15053  muldvds2  15054  dvdscmul  15055  dvdsmulc  15056  rpexp  15479  pospropd  17181  mdetmul  20477  elcls  20925  iscnp4  21115  cnpnei  21116  cnpflf2  21851  cnpflf  21852  cnpfcf  21892  xbln0  22266  blcls  22358  iimulcl  22783  icccvx  22796  iscau2  23121  rrxcph  23226  cncombf  23470  mumul  24952  ax5seglem1  25853  ax5seglem2  25854  clwwlkinwwlk  27003  wwlksext2clwwlkOLD  27022  nvmul0or  27633  fh1  28605  fh2  28606  cm2j  28607  pjoi0  28704  hoadddi  28790  hmopco  29010  padct  29625  iocinif  29671  volfiniune  30421  eulerpartlemb  30558  ivthALT  32455  cnambfre  33588  rngohomco  33903  rngoisoco  33911  pexmidlem3N  35576  hdmapglem7  37538  relexpmulg  38319  supxrgere  39862  supxrgelem  39866  supxrge  39867  infxr  39896  infleinflem2  39900  rexabslelem  39958  lptre2pt  40190  fnlimfvre  40224  limsupmnfuzlem  40276  climisp  40296  limsupgtlem  40327  dvnprodlem1  40479  ibliccsinexp  40484  iblioosinexp  40486  fourierdlem12  40654  fourierdlem41  40683  fourierdlem42  40684  fourierdlem48  40689  fourierdlem49  40690  fourierdlem51  40692  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem97  40738  etransclem24  40793  ioorrnopnlem  40842  issalnnd  40881  sge0rpcpnf  40956  sge0seq  40981  meaiuninc3v  41019  smfmullem4  41322  smflimsupmpt  41356  smfliminfmpt  41359  lincdifsn  42538
  Copyright terms: Public domain W3C validator