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  2656  2mo  2678  mosubopt  5484  predpoirr  6324  predfrirr  6325  funfv  6958  dffv2  6966  fvmptnf  7002  rdgsucmptnf  8404  frsucmptn  8414  mapdom2  9124  frfi  9233  oiexg  9485  wemapwe  9654  r1tr  9736  alephsing  10248  uzin  12889  fundmge2nop0  14529  fun2dmnop0  14531  wrdnfi  14575  relexpsucrd  15060  relexpsucld  15061  relexpreld  15067  relexpdmd  15071  relexprnd  15075  relexpfldd  15077  relexpaddd  15081  dfrtrclrec2  15085  rtrclreclem4  15088  dfrtrcl2  15089  relexpindlem  15090  sumrblem  15752  fsumcvg  15753  summolem2a  15756  fsumcvg2  15768  prodeq2ii  15955  prodrblem  15973  fprodcvg  15974  prodmolem2a  15978  zprod  15981  ptpjpre1  23689  qtopres  23816  fgabs  23997  ptcmplem3  24172  setsmstopn  24596  tngtopn  24768  cnmpopc  25048  pcoval2  25136  pcopt  25142  pcopt2  25143  itgle  25930  ibladdlem  25940  iblabslem  25948  iblabs  25949  iblabsr  25950  iblmulc2  25951  bddiblnc  25962  ditgneg  25977  logbgcd1irr  26917  umgr2adedgspth  30206  n4cyclfrgr  30551  poimirlem26  38157  poimirlem32  38163  ovoliunnfl  38173  voliunnfl  38175  volsupnfl  38176  itg2addnclem  38182  itg2gt0cn  38186  ibladdnclem  38187  iblabsnclem  38194  iblabsnc  38195  iblmulc2nc  38196  ftc1anclem7  38210  ftc1anclem8  38211  ftc1anc  38212  dicvalrelN  41821  dihvalrel  41915  pgn4cyclex  48746  ldepspr  49104  naryfval  49259  naryfvalixp  49260