Theorem pm2.61d1 182

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 181	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  186  ja  188  pm2.01d  192  moexexlem  2654  2mo  2676  mosubopt  5495  predpoirr  6336  predfrirr  6337  funfv  6970  dffv2  6978  fvmptnf  7014  rdgsucmptnf  8417  frsucmptn  8427  mapdom2  9137  frfi  9246  oiexg  9498  wemapwe  9667  r1tr  9749  alephsing  10261  uzin  12899  fundmge2nop0  14541  fun2dmnop0  14543  wrdnfi  14587  relexpsucrd  15072  relexpsucld  15073  relexpreld  15079  relexpdmd  15083  relexprnd  15087  relexpfldd  15089  relexpaddd  15093  dfrtrclrec2  15097  rtrclreclem4  15100  dfrtrcl2  15101  relexpindlem  15102  sumrblem  15764  fsumcvg  15765  summolem2a  15768  fsumcvg2  15780  prodeq2ii  15967  prodrblem  15985  fprodcvg  15986  prodmolem2a  15990  zprod  15993  ptpjpre1  23709  qtopres  23836  fgabs  24017  ptcmplem3  24192  setsmstopn  24616  tngtopn  24788  cnmpopc  25068  pcoval2  25156  pcopt  25162  pcopt2  25163  itgle  25950  ibladdlem  25960  iblabslem  25968  iblabs  25969  iblabsr  25970  iblmulc2  25971  bddiblnc  25982  ditgneg  25997  logbgcd1irr  26937  umgr2adedgspth  30275  n4cyclfrgr  30620  poimirlem26  38275  poimirlem32  38281  ovoliunnfl  38291  voliunnfl  38293  volsupnfl  38294  itg2addnclem  38300  itg2gt0cn  38304  ibladdnclem  38305  iblabsnclem  38312  iblabsnc  38313  iblmulc2nc  38314  ftc1anclem7  38328  ftc1anclem8  38329  ftc1anc  38330  dicvalrelN  41937  dihvalrel  42031  pgn4cyclex  48868  ldepspr  49230  naryfval  49385  naryfvalixp  49386