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 384
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 155 . . 3 (𝜑 → (¬ 𝜓 → ¬ 𝜒))
4 pm5.21ndd.2 . . . 4 (𝜑 → (𝜃𝜓))
54con3d 155 . . 3 (𝜑 → (¬ 𝜓 → ¬ 𝜃))
6 pm5.21im 378 . . 3 𝜒 → (¬ 𝜃 → (𝜒𝜃)))
73, 5, 6syl6c 70 . 2 (𝜑 → (¬ 𝜓 → (𝜒𝜃)))
81, 7pm2.61d 182 1 (𝜑 → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209
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 210
This theorem is referenced by:  pm5.21nd  801  sbcrext  3802  rmob  3819  elpr2g  4549  oteqex  5355  epelg  5431  eqbrrdva  5704  relbrcnvg  5935  ordsucuniel  7519  ordsucun  7520  brtpos2  7881  eceqoveq  8385  elpmg  8405  elfi2  8862  brwdom  9015  brwdomn0  9017  rankr1c  9234  r1pwcl  9260  ttukeylem1  9920  fpwwe2lem9  10049  eltskm  10254  recmulnq  10375  clim  14843  rlim  14844  lo1o1  14881  o1lo1  14886  o1lo12  14887  rlimresb  14914  lo1eq  14917  rlimeq  14918  isercolllem2  15014  caucvgb  15028  saddisj  15804  sadadd  15806  sadass  15810  bitsshft  15814  smupvallem  15822  smumul  15832  catpropd  16971  isssc  17082  issubc  17097  funcres2b  17159  funcres2c  17163  mndpropd  17928  issubg3  18289  resghm2b  18368  resscntz  18454  elsymgbas  18494  odmulg  18675  dmdprd  19113  dprdw  19125  subgdmdprd  19149  lmodprop2d  19689  lssacs  19732  prmirred  20188  lindfmm  20516  lsslindf  20519  islinds3  20523  assapropd  20558  psrbaglefi  20610  cnrest2  21891  cnprest  21894  cnprest2  21895  lmss  21903  isfildlem  22462  isfcls  22614  elutop  22839  metustel  23157  blval2  23169  dscopn  23180  iscau2  23881  causs  23902  ismbf  24232  ismbfcn  24233  iblcnlem  24392  limcdif  24479  limcres  24489  limcun  24498  dvres  24514  q1peqb  24755  ulmval  24975  ulmres  24983  chpchtsum  25803  dchrisum0lem1  26100  axcontlem5  26762  iswlkg  27403  issiga  31481  ismeas  31568  elcarsg  31673  cvmlift3lem4  32682  msrrcl  32903  brcolinear2  33632  topfneec  33816  bj-epelg  34484  cnpwstotbnd  35235  ismtyima  35241  ismndo2  35312  isrngo  35335  lshpkr  36413  elrfi  39633  climf  42262  climf2  42306  isupwlkg  44363
  Copyright terms: Public domain W3C validator