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  2654  2mo  2676  mosubopt  5486  mosubott  5488  predpoirr  6354  predfrirr  6355  funfv  6995  dffv2  7003  fvmptnf  7039  rdgsucmptnf  8465  frsucmptn  8475  mapdom2  9195  frfi  9304  oiexg  9556  wemapwe  9725  r1tr  9810  alephsing  10381  uzin  13028  fundmge2nop0  14674  fun2dmnop0  14676  wrdnfi  14720  relexpsucrd  15215  relexpsucld  15216  relexpreld  15222  relexpdmd  15226  relexprnd  15230  relexpfldd  15232  relexpaddd  15236  dfrtrclrec2  15240  rtrclreclem4  15243  dfrtrcl2  15244  relexpindlem  15245  sumrblem  15906  fsumcvg  15907  summolem2a  15910  fsumcvg2  15922  prodeq2ii  16109  prodrblem  16125  fprodcvg  16126  prodmolem2a  16130  zprod  16133  ptpjpre1  23920  qtopres  24047  fgabs  24228  ptcmplem3  24403  setsmstopn  24827  tngtopn  24999  cnmpopc  25279  pcoval2  25367  pcopt  25373  pcopt2  25374  itgle  26160  ibladdlem  26170  iblabslem  26178  iblabs  26179  iblabsr  26180  iblmulc2  26181  bddiblnc  26192  ditgneg  26207  logbgcd1irr  27152  umgr2adedgspth  30567  n4cyclfrgr  30922  poimirlem26  38756  poimirlem32  38762  ovoliunnfl  38772  voliunnfl  38774  volsupnfl  38775  itg2addnclem  38781  itg2gt0cn  38785  ibladdnclem  38786  iblabsnclem  38793  iblabsnc  38794  iblmulc2nc  38795  ftc1anclem7  38809  ftc1anclem8  38810  ftc1anc  38811  dicvalrelN  42434  dihvalrel  42528  pgn4cyclex  49429  ldepspr  49790  naryfval  49945  naryfvalixp  49946