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  2651  2mo  2673  mosubopt  5481  mosubott  5483  predpoirr  6336  predfrirr  6337  funfv  6972  dffv2  6980  fvmptnf  7016  rdgsucmptnf  8440  frsucmptn  8450  mapdom2  9170  frfi  9279  oiexg  9532  wemapwe  9701  r1tr  9786  alephsing  10357  uzin  13004  fundmge2nop0  14650  fun2dmnop0  14652  wrdnfi  14696  relexpsucrd  15191  relexpsucld  15192  relexpreld  15198  relexpdmd  15202  relexprnd  15206  relexpfldd  15208  relexpaddd  15212  dfrtrclrec2  15216  rtrclreclem4  15219  dfrtrcl2  15220  relexpindlem  15221  sumrblem  15882  fsumcvg  15883  summolem2a  15886  fsumcvg2  15898  prodeq2ii  16085  prodrblem  16101  fprodcvg  16102  prodmolem2a  16106  zprod  16109  ptpjpre1  23895  qtopres  24022  fgabs  24203  ptcmplem3  24378  setsmstopn  24802  tngtopn  24974  cnmpopc  25254  pcoval2  25342  pcopt  25348  pcopt2  25349  itgle  26135  ibladdlem  26145  iblabslem  26153  iblabs  26154  iblabsr  26155  iblmulc2  26156  bddiblnc  26167  ditgneg  26182  logbgcd1irr  27127  umgr2adedgspth  30542  n4cyclfrgr  30897  poimirlem26  38657  poimirlem32  38663  ovoliunnfl  38673  voliunnfl  38675  volsupnfl  38676  itg2addnclem  38682  itg2gt0cn  38686  ibladdnclem  38687  iblabsnclem  38694  iblabsnc  38695  iblmulc2nc  38696  ftc1anclem7  38710  ftc1anclem8  38711  ftc1anc  38712  dicvalrelN  42335  dihvalrel  42429  pgn4cyclex  49317  ldepspr  49678  naryfval  49833  naryfvalixp  49834