Theorem pm2.61d1 181

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

Step	Hyp	Ref	Expression
1		pm2.61d1.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		pm2.61d1.2	. . 3 ⊢ (¬ 𝜓 → 𝜒)
3	2	a1i 11	. 2 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
4	1, 3	pm2.61d 180	1 ⊢ (𝜑 → 𝜒)

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  185  ja  187  pm2.01d  191  moexexlem  2630  2mo  2652  mosubopt  5458  predpoirr  6291  predfrirr  6292  funfv  6921  dffv2  6929  fvmptnf  6965  rdgsucmptnf  8365  frsucmptn  8375  mapdom2  9083  frfi  9192  oiexg  9447  wemapwe  9616  r1tr  9698  alephsing  10196  uzin  12822  fundmge2nop0  14462  fun2dmnop0  14464  wrdnfi  14508  relexpsucrd  14993  relexpsucld  14994  relexpreld  15000  relexpdmd  15004  relexprnd  15008  relexpfldd  15010  relexpaddd  15014  dfrtrclrec2  15018  rtrclreclem4  15021  dfrtrcl2  15022  relexpindlem  15023  sumrblem  15671  fsumcvg  15672  summolem2a  15675  fsumcvg2  15687  prodeq2ii  15874  prodrblem  15892  fprodcvg  15893  prodmolem2a  15897  zprod  15900  ptpjpre1  23561  qtopres  23688  fgabs  23869  ptcmplem3  24044  setsmstopn  24468  tngtopn  24640  cnmpopc  24920  pcoval2  25008  pcopt  25014  pcopt2  25015  itgle  25802  ibladdlem  25812  iblabslem  25820  iblabs  25821  iblabsr  25822  iblmulc2  25823  bddiblnc  25834  ditgneg  25849  logbgcd1irr  26783  umgr2adedgspth  30041  n4cyclfrgr  30386  poimirlem26  38020  poimirlem32  38026  ovoliunnfl  38036  voliunnfl  38038  volsupnfl  38039  itg2addnclem  38045  itg2gt0cn  38049  ibladdnclem  38050  iblabsnclem  38057  iblabsnc  38058  iblmulc2nc  38059  ftc1anclem7  38073  ftc1anclem8  38074  ftc1anc  38075  dicvalrelN  41684  dihvalrel  41778  pgn4cyclex  48624  ldepspr  48971  naryfval  49126  naryfvalixp  49127