Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-ceqsalt0 Structured version   Unicode version

Theorem bj-ceqsalt0 33931
Description: The FOL content of ceqsalt 3141. Lemma for bj-ceqsalt 33933 and bj-ceqsaltv 33934. (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.)
Assertion
Ref Expression
bj-ceqsalt0  |-  ( ( F/ x ps  /\  A. x ( th  ->  (
ph 
<->  ps ) )  /\  E. x th )  -> 
( A. x ( th  ->  ph )  <->  ps )
)

Proof of Theorem bj-ceqsalt0
StepHypRef Expression
1 simp3 998 . . 3  |-  ( ( F/ x ps  /\  A. x ( th  ->  (
ph 
<->  ps ) )  /\  E. x th )  ->  E. x th )
2 bi1 186 . . . . . . 7  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
32imim3i 59 . . . . . 6  |-  ( ( th  ->  ( ph  <->  ps ) )  ->  (
( th  ->  ph )  ->  ( th  ->  ps ) ) )
43al2imi 1616 . . . . 5  |-  ( A. x ( th  ->  (
ph 
<->  ps ) )  -> 
( A. x ( th  ->  ph )  ->  A. x ( th  ->  ps ) ) )
543ad2ant2 1018 . . . 4  |-  ( ( F/ x ps  /\  A. x ( th  ->  (
ph 
<->  ps ) )  /\  E. x th )  -> 
( A. x ( th  ->  ph )  ->  A. x ( th  ->  ps ) ) )
6 19.23t 1856 . . . . 5  |-  ( F/ x ps  ->  ( A. x ( th  ->  ps )  <->  ( E. x th  ->  ps ) ) )
763ad2ant1 1017 . . . 4  |-  ( ( F/ x ps  /\  A. x ( th  ->  (
ph 
<->  ps ) )  /\  E. x th )  -> 
( A. x ( th  ->  ps )  <->  ( E. x th  ->  ps ) ) )
85, 7sylibd 214 . . 3  |-  ( ( F/ x ps  /\  A. x ( th  ->  (
ph 
<->  ps ) )  /\  E. x th )  -> 
( A. x ( th  ->  ph )  -> 
( E. x th  ->  ps ) ) )
91, 8mpid 41 . 2  |-  ( ( F/ x ps  /\  A. x ( th  ->  (
ph 
<->  ps ) )  /\  E. x th )  -> 
( A. x ( th  ->  ph )  ->  ps ) )
10 bi2 198 . . . . . . 7  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )
1110imim2i 14 . . . . . 6  |-  ( ( th  ->  ( ph  <->  ps ) )  ->  ( th  ->  ( ps  ->  ph ) ) )
1211com23 78 . . . . 5  |-  ( ( th  ->  ( ph  <->  ps ) )  ->  ( ps  ->  ( th  ->  ph ) ) )
1312alimi 1614 . . . 4  |-  ( A. x ( th  ->  (
ph 
<->  ps ) )  ->  A. x ( ps  ->  ( th  ->  ph ) ) )
14133ad2ant2 1018 . . 3  |-  ( ( F/ x ps  /\  A. x ( th  ->  (
ph 
<->  ps ) )  /\  E. x th )  ->  A. x ( ps  ->  ( th  ->  ph ) ) )
15 19.21t 1852 . . . 4  |-  ( F/ x ps  ->  ( A. x ( ps  ->  ( th  ->  ph ) )  <-> 
( ps  ->  A. x
( th  ->  ph )
) ) )
16153ad2ant1 1017 . . 3  |-  ( ( F/ x ps  /\  A. x ( th  ->  (
ph 
<->  ps ) )  /\  E. x th )  -> 
( A. x ( ps  ->  ( th  ->  ph ) )  <->  ( ps  ->  A. x ( th 
->  ph ) ) ) )
1714, 16mpbid 210 . 2  |-  ( ( F/ x ps  /\  A. x ( th  ->  (
ph 
<->  ps ) )  /\  E. x th )  -> 
( ps  ->  A. x
( th  ->  ph )
) )
189, 17impbid 191 1  |-  ( ( F/ x ps  /\  A. x ( th  ->  (
ph 
<->  ps ) )  /\  E. x th )  -> 
( A. x ( th  ->  ph )  <->  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 973   A.wal 1377   E.wex 1596   F/wnf 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-ex 1597  df-nf 1600
This theorem is referenced by:  bj-ceqsalt  33933  bj-ceqsaltv  33934  bj-ceqsalg0  33935
  Copyright terms: Public domain W3C validator