Theorem pm2.21d 121

Description: A contradiction implies anything. Deduction associated with pm2.21 123. (Contributed by NM, 10-Feb-1996.)

Hypothesis

Ref	Expression
pm2.21d.1	⊢ (𝜑 → ¬ 𝜓)

Assertion

Ref	Expression
pm2.21d	⊢ (𝜑 → (𝜓 → 𝜒))

Proof of Theorem pm2.21d

Step	Hyp	Ref	Expression
1		pm2.21d.1	. . 3 ⊢ (𝜑 → ¬ 𝜓)
2	1	a1d 25	. 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	con4d 115	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.21ddALT  122  pm2.21  123  pm2.521g  174  prlem1  1054  sbc2or  3799  eq0rdvALT  4413  rzalALT  4515  reusv2lem2  5404  po2ne  5612  poirr2  6146  sofld  6208  dfwe2  7792  tfindsg  7881  findsg  7919  omopth2  8620  swoord2  8776  unxpdomlem3  9285  preleqg  9652  suc11reg  9656  wemapwe  9734  r111  9812  r1pwss  9821  cflim2  10300  axunndlem1  10632  axunnd  10633  axpowndlem3  10636  axpownd  10638  axregndlem1  10639  axregndlem2  10640  axinfndlem1  10642  axinfnd  10643  axacndlem1  10644  axacndlem2  10645  axacndlem3  10646  axacndlem4  10647  axacndlem5  10648  axacnd  10649  fpwwe2lem12  10679  gchpwdom  10707  winalim2  10733  ltapr  11082  prodgt0  12111  squeeze0  12168  nnsub  12307  nn0sub  12573  elnnz  12620  nn0lt10b  12677  indstr2  12966  uzsupss  12979  nn01to3  12980  xrltnsym  13175  xrlttr  13178  qbtwnxr  13238  xltnegi  13254  xmullem  13302  xlemul1a  13326  xrsupsslem  13345  xrinfmsslem  13346  xrub  13350  xrsup0  13361  xrinf0  13376  reltxrnmnf  13380  ixxdisj  13398  icodisj  13512  fzm1  13643  addmodlteq  13983  facdiv  14322  hasheqf1oi  14386  relexpfld  15084  relexpuzrel  15087  reusq0  15497  climuni  15584  rlimno1  15686  sqrt2irr  16281  nn0rppwr  16594  prmdvdsexpr  16750  prmfac1  16753  dvdsprmpweqle  16919  ramlb  17052  ram0  17055  prmgaplem6  17089  prmlem1  17141  prmlem2  17153  pospo  18402  efgredlemc  19777  efgred  19780  ablsimpnosubgd  20138  sdrgacs  20818  prmirred  21502  psrvscafval  21985  fvmptnn04ifa  22871  fvmptnn04ifb  22872  fvmptnn04ifc  22873  fvmptnn04ifd  22874  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  0top  23005  pnfnei  23243  mnfnei  23244  cmpfi  23431  1stccnp  23485  filconn  23906  ivthlem2  25500  ivthlem3  25501  ovolicc2lem3  25567  itg1addlem4  25747  itg1addlem4OLD  25748  itg2seq  25791  dvcnvlem  26028  lhop2  26068  bpos1  27341  lgsdir2lem2  27384  lgsqrlem2  27405  lgseisenlem2  27434  2sqnn  27497  pntlem3  27667  ostth3  27696  nosupbnd1lem5  27771  noinfbnd1lem5  27786  noetasuplem4  27795  noetainflem4  27799  elnnzs  28401  expsne0  28428  tgcgr4  28553  axlowdimlem15  28985  nbusgrvtxm1  29410  wlkv0  29683  1to2vfriswmgr  30307  n4cyclfrgr  30319  frgrnbnb  30321  frgrregord013  30423  snsssng  32541  ifeqeqx  32562  rprmdvdsprod  33541  fldext2chn  33733  f1resrcmplf1dlem  35078  erdszelem4  35178  erdszelem8  35182  finminlem  36300  nn0prpwlem  36304  nn0prpw  36305  ordcmp  36429  iooelexlt  37344  relowlssretop  37345  smprngopr  38038  disjlem14  38779  prtlem14  38855  atltcvr  39417  dihord6apre  41238  dihord6b  41242  jm2.23  42984  onexlimgt  43231  ordnexbtwnsuc  43256  onov0suclim  43263  relexpmulg  43699  rzalf  44954  or2expropbi  46983  icceuelpart  47360  iccpartnel  47362  poprelb  47448  goldbachthlem2  47470  fmtnoprmfac1  47489  fmtnoprmfac2  47491  fmtno4prmfac  47496  fmtno4prmfac193  47497  2pwp1prm  47513  lighneallem4  47534  requad1  47546  requad2  47547  evenprm2  47638  odd2prm2  47642  stgoldbwt  47700  sbgoldbwt  47701  sbgoldbalt  47705  usgrexmpl12ngric  47932  ztprmneprm  48191