MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm5.21ndd Structured version   Visualization version   GIF version

Theorem pm5.21ndd 368
Description: Eliminate an antecedent implied by each side of a biconditional, deduction version. (Contributed by Paul Chapman, 21-Nov-2012.) (Proof shortened by Wolf Lammen, 6-Oct-2013.)
Hypotheses
Ref Expression
pm5.21ndd.1 (𝜑 → (𝜒𝜓))
pm5.21ndd.2 (𝜑 → (𝜃𝜓))
pm5.21ndd.3 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
pm5.21ndd (𝜑 → (𝜒𝜃))

Proof of Theorem pm5.21ndd
StepHypRef Expression
1 pm5.21ndd.3 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
2 pm5.21ndd.1 . . . 4 (𝜑 → (𝜒𝜓))
32con3d 147 . . 3 (𝜑 → (¬ 𝜓 → ¬ 𝜒))
4 pm5.21ndd.2 . . . 4 (𝜑 → (𝜃𝜓))
54con3d 147 . . 3 (𝜑 → (¬ 𝜓 → ¬ 𝜃))
6 pm5.21im 363 . . 3 𝜒 → (¬ 𝜃 → (𝜒𝜃)))
73, 5, 6syl6c 68 . 2 (𝜑 → (¬ 𝜓 → (𝜒𝜃)))
81, 7pm2.61d 169 1 (𝜑 → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 196
This theorem is referenced by:  pm5.21nd  939  sbcrext  3478  rmob  3495  oteqex  4889  epelg  4950  eqbrrdva  5213  relbrcnvg  5423  ordsucuniel  6916  ordsucun  6917  brtpos2  7245  eceqoveq  7740  elpmg  7759  elfi2  8203  brwdom  8355  brwdomn0  8357  rankr1c  8567  r1pwcl  8593  ttukeylem1  9214  fpwwe2lem9  9339  eltskm  9544  recmulnq  9665  clim  14073  rlim  14074  lo1o1  14111  o1lo1  14116  o1lo12  14117  rlimresb  14144  lo1eq  14147  rlimeq  14148  isercolllem2  14244  caucvgb  14258  saddisj  15025  sadadd  15027  sadass  15031  bitsshft  15035  smupvallem  15043  smumul  15053  catpropd  16192  isssc  16303  issubc  16318  funcres2b  16380  funcres2c  16384  mndpropd  17139  issubg3  17435  resghm2b  17501  resscntz  17587  elsymgbas  17625  odmulg  17796  dmdprd  18220  dprdw  18232  subgdmdprd  18256  lmodprop2d  18748  lssacs  18788  assapropd  19148  psrbaglefi  19193  prmirred  19662  lindfmm  19985  lsslindf  19988  islinds3  19992  cnrest2  20900  cnprest  20903  cnprest2  20904  lmss  20912  isfildlem  21471  isfcls  21623  elutop  21847  metustel  22165  blval2  22177  dscopn  22188  iscau2  22883  causs  22904  ismbf  23203  ismbfcn  23204  iblcnlem  23361  limcdif  23446  limcres  23456  limcun  23465  dvres  23481  q1peqb  23718  ulmval  23938  ulmres  23946  chpchtsum  24744  dchrisum0lem1  25005  axcontlem5  25648  iseupa  26492  issiga  29501  ismeas  29589  elcarsg  29694  cvmlift3lem4  30558  msrrcl  30694  brcolinear2  31335  topfneec  31520  cnpwstotbnd  32766  ismtyima  32772  ismndo2  32843  isrngo  32866  lshpkr  33422  elrfi  36275  climf  38689  climf2  38733  is1wlkg  40816
  Copyright terms: Public domain W3C validator