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  2623  2mo  2645  mosubopt  5453  predpoirr  6285  predfrirr  6286  funfv  6915  dffv2  6923  fvmptnf  6957  rdgsucmptnf  8354  frsucmptn  8364  mapdom2  9068  frfi  9176  oiexg  9428  wemapwe  9594  r1tr  9676  alephsing  10174  uzin  12774  fundmge2nop0  14411  fun2dmnop0  14413  wrdnfi  14457  relexpsucrd  14942  relexpsucld  14943  relexpreld  14949  relexpdmd  14953  relexprnd  14957  relexpfldd  14959  relexpaddd  14963  dfrtrclrec2  14967  rtrclreclem4  14970  dfrtrcl2  14971  relexpindlem  14972  sumrblem  15620  fsumcvg  15621  summolem2a  15624  fsumcvg2  15636  prodeq2ii  15820  prodrblem  15838  fprodcvg  15839  prodmolem2a  15843  zprod  15846  ptpjpre1  23487  qtopres  23614  fgabs  23795  ptcmplem3  23970  setsmstopn  24394  tngtopn  24566  cnmpopc  24850  pcoval2  24944  pcopt  24950  pcopt2  24951  itgle  25739  ibladdlem  25749  iblabslem  25757  iblabs  25758  iblabsr  25759  iblmulc2  25760  bddiblnc  25771  ditgneg  25786  logbgcd1irr  26732  umgr2adedgspth  29928  n4cyclfrgr  30273  poimirlem26  37707  poimirlem32  37713  ovoliunnfl  37723  voliunnfl  37725  volsupnfl  37726  itg2addnclem  37732  itg2gt0cn  37736  ibladdnclem  37737  iblabsnclem  37744  iblabsnc  37745  iblmulc2nc  37746  ftc1anclem7  37760  ftc1anclem8  37761  ftc1anc  37762  dicvalrelN  41305  dihvalrel  41399  pgn4cyclex  48251  ldepspr  48599  naryfval  48754  naryfvalixp  48755