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

Theorem aleximi 1715
Description: A variant of al2imi 1698: instead of applying  A. x quantifiers to the final implication, replace them with  E. x. A shorter proof is possible using nfa1 1990, sps 1954 and eximd 1971, 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 140 . . . 4  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32al2imi 1698 . . 3  |-  ( A. x ph  ->  ( A. x  -.  ch  ->  A. x  -.  ps ) )
4 alnex 1676 . . 3  |-  ( A. x  -.  ch  <->  -.  E. x ch )
5 alnex 1676 . . 3  |-  ( A. x  -.  ps  <->  -.  E. x ps )
63, 4, 53imtr3g 277 . 2  |-  ( A. x ph  ->  ( -.  E. x ch  ->  -.  E. x ps ) )
76con4d 109 1  |-  ( A. x ph  ->  ( E. x ps  ->  E. x ch ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1453   E.wex 1674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693
This theorem depends on definitions:  df-bi 190  df-ex 1675
This theorem is referenced by:  alexbii  1716  exim  1717  exbiOLD  1728  eximdh  1735  19.29  1746  19.29r  1747  19.35  1751  19.25  1754  19.30  1755  19.40b  1761  speimfw  1804  aev  2037  2ax6elem  2289  mo3  2347  mopick  2375  2mo  2391  eleq2dOLD  2526  ssopab2  4741  opabbrexOLD  6358  ssoprab2  6374  axextnd  9042  bj-2exim  31248  bj-exaleximi  31269  bj-sb56  31297  wl-mo3t  31950  pm10.56  36763  2exim  36772
  Copyright terms: Public domain W3C validator