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

Theorem aleximi 1653
Description: A variant of al2imi 1636: instead of applying A.x quantifiers to the final implication, replace them with E.x. A shorter proof is possible using nfa1 1897, sps 1865 and eximd 1882, but it depends on more axioms. (Contributed by Wolf Lammen, 18-Aug-2019.)
Hypothesis
Ref Expression
aleximi.1
Assertion
Ref Expression
aleximi

Proof of Theorem aleximi
StepHypRef Expression
1 aleximi.1 . . . . 5
21con3d 133 . . . 4
32al2imi 1636 . . 3
4 alnex 1614 . . 3
5 alnex 1614 . . 3
63, 4, 53imtr3g 269 . 2
76con4d 105 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  A.wal 1393  E.wex 1612
This theorem is referenced by:  exim  1654  exbi  1666  eximdh  1673  19.29  1683  19.35  1687  19.25  1691  19.30  1692  speimfw  1735  aev  1943  2ax6elem  2193  mo3  2323  mopick  2356  2mo  2373  2moOLD  2374  eleq2d  2527  ssopab2  4778  opabbrexOLD  6340  ssoprab2  6353  axextnd  8987  wl-mo3t  30021  pm10.56  31275  2exim  31284  bj-2exim  34203
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator