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  2627  2mo  2649  mosubopt  5458  predpoirr  6291  predfrirr  6292  funfv  6921  dffv2  6929  fvmptnf  6964  rdgsucmptnf  8361  frsucmptn  8371  mapdom2  9079  frfi  9188  oiexg  9443  wemapwe  9609  r1tr  9691  alephsing  10189  uzin  12815  fundmge2nop0  14455  fun2dmnop0  14457  wrdnfi  14501  relexpsucrd  14986  relexpsucld  14987  relexpreld  14993  relexpdmd  14997  relexprnd  15001  relexpfldd  15003  relexpaddd  15007  dfrtrclrec2  15011  rtrclreclem4  15014  dfrtrcl2  15015  relexpindlem  15016  sumrblem  15664  fsumcvg  15665  summolem2a  15668  fsumcvg2  15680  prodeq2ii  15867  prodrblem  15885  fprodcvg  15886  prodmolem2a  15890  zprod  15893  ptpjpre1  23546  qtopres  23673  fgabs  23854  ptcmplem3  24029  setsmstopn  24453  tngtopn  24625  cnmpopc  24905  pcoval2  24993  pcopt  24999  pcopt2  25000  itgle  25787  ibladdlem  25797  iblabslem  25805  iblabs  25806  iblabsr  25807  iblmulc2  25808  bddiblnc  25819  ditgneg  25834  logbgcd1irr  26771  umgr2adedgspth  30031  n4cyclfrgr  30376  poimirlem26  37981  poimirlem32  37987  ovoliunnfl  37997  voliunnfl  37999  volsupnfl  38000  itg2addnclem  38006  itg2gt0cn  38010  ibladdnclem  38011  iblabsnclem  38018  iblabsnc  38019  iblmulc2nc  38020  ftc1anclem7  38034  ftc1anclem8  38035  ftc1anc  38036  dicvalrelN  41645  dihvalrel  41739  pgn4cyclex  48614  ldepspr  48961  naryfval  49116  naryfvalixp  49117