Theorem pm2.61d1 180

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 179	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  184  ja  186  pm2.01d  190  moexexlem  2619  2mo  2641  mosubopt  5470  predpoirr  6306  predfrirr  6307  funfv  6948  dffv2  6956  fvmptnf  6990  rdgsucmptnf  8397  frsucmptn  8407  mapdom2  9112  frfi  9232  oiexg  9488  wemapwe  9650  r1tr  9729  alephsing  10229  uzin  12833  fundmge2nop0  14467  fun2dmnop0  14469  wrdnfi  14513  relexpsucrd  14999  relexpsucld  15000  relexpreld  15006  relexpdmd  15010  relexprnd  15014  relexpfldd  15016  relexpaddd  15020  dfrtrclrec2  15024  rtrclreclem4  15027  dfrtrcl2  15028  relexpindlem  15029  sumrblem  15677  fsumcvg  15678  summolem2a  15681  fsumcvg2  15693  prodeq2ii  15877  prodrblem  15895  fprodcvg  15896  prodmolem2a  15900  zprod  15903  ptpjpre1  23458  qtopres  23585  fgabs  23766  ptcmplem3  23941  setsmstopn  24366  tngtopn  24538  cnmpopc  24822  pcoval2  24916  pcopt  24922  pcopt2  24923  itgle  25711  ibladdlem  25721  iblabslem  25729  iblabs  25730  iblabsr  25731  iblmulc2  25732  bddiblnc  25743  ditgneg  25758  logbgcd1irr  26704  umgr2adedgspth  29878  n4cyclfrgr  30220  poimirlem26  37640  poimirlem32  37646  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  itg2addnclem  37665  itg2gt0cn  37669  ibladdnclem  37670  iblabsnclem  37677  iblabsnc  37678  iblmulc2nc  37679  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  dicvalrelN  41179  dihvalrel  41273  pgn4cyclex  48116  ldepspr  48462  naryfval  48617  naryfvalixp  48618