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

 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 1145 . 2 ((𝜑𝜓𝜏) → (𝜑𝜓))
2 3adantl.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 583 1 (((𝜑𝜓𝜏) ∧ 𝜒) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  dif1en  8739  infpssrlem4  9717  fin23lem11  9728  tskwun  10195  gruf  10222  lediv2a  11523  prunioo  12859  nn0p1elfzo  13075  hashunsnggt  13751  rpnnen2lem7  15564  muldvds1  15625  muldvds2  15626  dvdscmul  15627  dvdsmulc  15628  rpexp  16053  pospropd  17735  mdetmul  21226  elcls  21676  iscnp4  21866  cnpnei  21867  cnpflf2  22603  cnpflf  22604  cnpfcf  22644  xbln0  23019  blcls  23111  iimulcl  23540  icccvx  23553  iscau2  23879  rrxcph  23994  cncombf  24260  mumul  25764  ax5seglem1  26720  ax5seglem2  26721  wwlksnext  27677  clwwlkinwwlk  27823  nvmul0or  28431  fh1  29399  fh2  29400  cm2j  29401  pjoi0  29498  hoadddi  29584  hmopco  29804  padct  30465  iocinif  30514  volfiniune  31563  eulerpartlemb  31700  ivthALT  33757  lindsadd  35008  cnambfre  35063  rngohomco  35370  rngoisoco  35378  pexmidlem3N  37226  hdmapglem7  39183  factwoffsmonot  39338  relexpmulg  40341  supxrgere  41904  supxrgelem  41908  supxrge  41909  infxr  41938  infleinflem2  41942  rexabslelem  41994  lptre2pt  42221  fnlimfvre  42255  limsupmnfuzlem  42307  climisp  42327  limsupgtlem  42358  dvnprodlem1  42527  ibliccsinexp  42532  iblioosinexp  42534  fourierdlem12  42700  fourierdlem41  42729  fourierdlem42  42730  fourierdlem48  42735  fourierdlem49  42736  fourierdlem51  42738  fourierdlem73  42760  fourierdlem74  42761  fourierdlem75  42762  fourierdlem97  42784  etransclem24  42839  ioorrnopnlem  42885  issalnnd  42924  sge0rpcpnf  42999  sge0seq  43024  meaiuninc3v  43062  smfmullem4  43365  smflimsupmpt  43399  smfliminfmpt  43402  lincdifsn  44772
 Copyright terms: Public domain W3C validator