MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.61d1 Structured version   Visualization version   GIF version

Theorem pm2.61d1 183
Description: Inference eliminating an antecedent. (Contributed by NM, 15-Jul-2005.)
Hypotheses
Ref Expression
pm2.61d1.1 (𝜑 → (𝜓𝜒))
pm2.61d1.2 𝜓𝜒)
Assertion
Ref Expression
pm2.61d1 (𝜑𝜒)

Proof of Theorem pm2.61d1
StepHypRef Expression
1 pm2.61d1.1 . 2 (𝜑 → (𝜓𝜒))
2 pm2.61d1.2 . . 3 𝜓𝜒)
32a1i 11 . 2 (𝜑 → (¬ 𝜓𝜒))
41, 3pm2.61d 182 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  pm2.61nii  187  ja  189  pm2.01d  193  moexexlem  2688  2mo  2710  mosubopt  5365  predpoirr  6144  predfrirr  6145  funfv  6725  dffv2  6733  fvmptnf  6767  rdgsucmptnf  8048  frsucmptn  8057  mapdom2  8672  frfi  8747  oiexg  8983  wemapwe  9144  r1tr  9189  alephsing  9687  uzin  12266  fundmge2nop0  13846  fun2dmnop0  13848  wrdnfi  13891  relexpsucrd  14384  relexpsucld  14385  relexpreld  14391  relexpdmd  14395  relexprnd  14399  relexpfldd  14401  relexpaddd  14405  dfrtrclrec2  14409  rtrclreclem4  14412  dfrtrcl2  14413  relexpindlem  14414  sumrblem  15060  fsumcvg  15061  summolem2a  15064  fsumcvg2  15076  prodeq2ii  15259  prodrblem  15275  fprodcvg  15276  prodmolem2a  15280  zprod  15283  ptpjpre1  22176  qtopres  22303  fgabs  22484  ptcmplem3  22659  setsmstopn  23085  tngtopn  23256  cnmpopc  23533  pcoval2  23621  pcopt  23627  pcopt2  23628  itgle  24413  ibladdlem  24423  iblabslem  24431  iblabs  24432  iblabsr  24433  iblmulc2  24434  bddiblnc  24445  ditgneg  24460  logbgcd1irr  25380  umgr2adedgspth  27734  n4cyclfrgr  28076  poimirlem26  35080  poimirlem32  35086  ovoliunnfl  35096  voliunnfl  35098  volsupnfl  35099  itg2addnclem  35105  itg2gt0cn  35109  ibladdnclem  35110  iblabsnclem  35117  iblabsnc  35118  iblmulc2nc  35119  ftc1anclem7  35133  ftc1anclem8  35134  ftc1anc  35135  dicvalrelN  38478  dihvalrel  38572  ldepspr  44877  naryfval  45037  naryfvalixp  45038
  Copyright terms: Public domain W3C validator