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 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.61nii  186  ja  188  pm2.01d  192  moexexlem  2657  2mo  2679  mosubopt  5498  predpoirr  6341  predfrirr  6342  funfv  6975  dffv2  6983  fvmptnf  7019  rdgsucmptnf  8425  frsucmptn  8435  mapdom2  9146  frfi  9255  oiexg  9507  wemapwe  9676  r1tr  9758  alephsing  10278  uzin  12916  fundmge2nop0  14559  fun2dmnop0  14561  wrdnfi  14605  relexpsucrd  15096  relexpsucld  15097  relexpreld  15103  relexpdmd  15107  relexprnd  15111  relexpfldd  15113  relexpaddd  15117  dfrtrclrec2  15121  rtrclreclem4  15124  dfrtrcl2  15125  relexpindlem  15126  sumrblem  15788  fsumcvg  15789  summolem2a  15792  fsumcvg2  15804  prodeq2ii  15991  prodrblem  16009  fprodcvg  16010  prodmolem2a  16014  zprod  16017  ptpjpre1  23765  qtopres  23892  fgabs  24073  ptcmplem3  24248  setsmstopn  24672  tngtopn  24844  cnmpopc  25124  pcoval2  25212  pcopt  25218  pcopt2  25219  itgle  26006  ibladdlem  26016  iblabslem  26024  iblabs  26025  iblabsr  26026  iblmulc2  26027  bddiblnc  26038  ditgneg  26053  logbgcd1irr  26996  umgr2adedgspth  30334  n4cyclfrgr  30679  poimirlem26  38338  poimirlem32  38344  ovoliunnfl  38354  voliunnfl  38356  volsupnfl  38357  itg2addnclem  38363  itg2gt0cn  38367  ibladdnclem  38368  iblabsnclem  38375  iblabsnc  38376  iblmulc2nc  38377  ftc1anclem7  38391  ftc1anclem8  38392  ftc1anc  38393  dicvalrelN  42000  dihvalrel  42094  pgn4cyclex  48932  ldepspr  49294  naryfval  49449  naryfvalixp  49450