MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  aleximi Structured version   Unicode version

Theorem aleximi 1698
Description: A variant of al2imi 1681: instead of applying  A. x quantifiers to the final implication, replace them with  E. x. A shorter proof is possible using nfa1 1956, sps 1920 and eximd 1937, but it depends on more axioms. (Contributed by Wolf Lammen, 18-Aug-2019.)
Hypothesis
Ref Expression
aleximi.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
aleximi  |-  ( A. x ph  ->  ( E. x ps  ->  E. x ch ) )

Proof of Theorem aleximi
StepHypRef Expression
1 aleximi.1 . . . . 5  |-  ( ph  ->  ( ps  ->  ch ) )
21con3d 138 . . . 4  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32al2imi 1681 . . 3  |-  ( A. x ph  ->  ( A. x  -.  ch  ->  A. x  -.  ps ) )
4 alnex 1659 . . 3  |-  ( A. x  -.  ch  <->  -.  E. x ch )
5 alnex 1659 . . 3  |-  ( A. x  -.  ps  <->  -.  E. x ps )
63, 4, 53imtr3g 272 . 2  |-  ( A. x ph  ->  ( -.  E. x ch  ->  -.  E. x ps ) )
76con4d 108 1  |-  ( A. x ph  ->  ( E. x ps  ->  E. x ch ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1435   E.wex 1657
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676
This theorem depends on definitions:  df-bi 188  df-ex 1658
This theorem is referenced by:  alexbii  1699  exim  1700  exbiOLD  1711  eximdh  1718  19.29  1729  19.29r  1730  19.35  1734  19.25  1737  19.30  1738  19.40b  1744  speimfw  1786  aev  2003  2ax6elem  2248  mo3  2306  mopick  2334  2mo  2350  eleq2dOLD  2493  ssopab2  4746  opabbrexOLD  6348  ssoprab2  6361  axextnd  9023  bj-2exim  31202  bj-exaleximi  31223  wl-mo3t  31869  pm10.56  36689  2exim  36698
  Copyright terms: Public domain W3C validator