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  2626  2mo  2648  mosubopt  5515  predpoirr  6354  predfrirr  6355  funfv  6996  dffv2  7004  fvmptnf  7038  rdgsucmptnf  8469  frsucmptn  8479  mapdom2  9188  frfi  9321  oiexg  9575  wemapwe  9737  r1tr  9816  alephsing  10316  uzin  12918  fundmge2nop0  14541  fun2dmnop0  14543  wrdnfi  14586  relexpsucrd  15072  relexpsucld  15073  relexpreld  15079  relexpdmd  15083  relexprnd  15087  relexpfldd  15089  relexpaddd  15093  dfrtrclrec2  15097  rtrclreclem4  15100  dfrtrcl2  15101  relexpindlem  15102  sumrblem  15747  fsumcvg  15748  summolem2a  15751  fsumcvg2  15763  prodeq2ii  15947  prodrblem  15965  fprodcvg  15966  prodmolem2a  15970  zprod  15973  ptpjpre1  23579  qtopres  23706  fgabs  23887  ptcmplem3  24062  setsmstopn  24490  tngtopn  24671  cnmpopc  24955  pcoval2  25049  pcopt  25055  pcopt2  25056  itgle  25845  ibladdlem  25855  iblabslem  25863  iblabs  25864  iblabsr  25865  iblmulc2  25866  bddiblnc  25877  ditgneg  25892  logbgcd1irr  26837  umgr2adedgspth  29968  n4cyclfrgr  30310  poimirlem26  37653  poimirlem32  37659  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  itg2addnclem  37678  itg2gt0cn  37682  ibladdnclem  37683  iblabsnclem  37690  iblabsnc  37691  iblmulc2nc  37692  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  dicvalrelN  41187  dihvalrel  41281  ldepspr  48390  naryfval  48549  naryfvalixp  48550