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

Theorem bj-ceqsalt0 31482
Description: The FOL content of ceqsalt 3070. Lemma for bj-ceqsalt 31484 and bj-ceqsaltv 31485. (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 1010 . . 3  |-  ( ( F/ x ps  /\  A. x ( th  ->  (
ph 
<->  ps ) )  /\  E. x th )  ->  E. x th )
2 biimp 197 . . . . . . 7  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
32imim3i 61 . . . . . 6  |-  ( ( th  ->  ( ph  <->  ps ) )  ->  (
( th  ->  ph )  ->  ( th  ->  ps ) ) )
43al2imi 1687 . . . . 5  |-  ( A. x ( th  ->  (
ph 
<->  ps ) )  -> 
( A. x ( th  ->  ph )  ->  A. x ( th  ->  ps ) ) )
543ad2ant2 1030 . . . 4  |-  ( ( F/ x ps  /\  A. x ( th  ->  (
ph 
<->  ps ) )  /\  E. x th )  -> 
( A. x ( th  ->  ph )  ->  A. x ( th  ->  ps ) ) )
6 19.23t 1991 . . . . 5  |-  ( F/ x ps  ->  ( A. x ( th  ->  ps )  <->  ( E. x th  ->  ps ) ) )
763ad2ant1 1029 . . . 4  |-  ( ( F/ x ps  /\  A. x ( th  ->  (
ph 
<->  ps ) )  /\  E. x th )  -> 
( A. x ( th  ->  ps )  <->  ( E. x th  ->  ps ) ) )
85, 7sylibd 218 . . 3  |-  ( ( F/ x ps  /\  A. x ( th  ->  (
ph 
<->  ps ) )  /\  E. x th )  -> 
( A. x ( th  ->  ph )  -> 
( E. x th  ->  ps ) ) )
91, 8mpid 42 . 2  |-  ( ( F/ x ps  /\  A. x ( th  ->  (
ph 
<->  ps ) )  /\  E. x th )  -> 
( A. x ( th  ->  ph )  ->  ps ) )
10 biimpr 202 . . . . . . 7  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )
1110imim2i 16 . . . . . 6  |-  ( ( th  ->  ( ph  <->  ps ) )  ->  ( th  ->  ( ps  ->  ph ) ) )
1211com23 81 . . . . 5  |-  ( ( th  ->  ( ph  <->  ps ) )  ->  ( ps  ->  ( th  ->  ph ) ) )
1312alimi 1684 . . . 4  |-  ( A. x ( th  ->  (
ph 
<->  ps ) )  ->  A. x ( ps  ->  ( th  ->  ph ) ) )
14133ad2ant2 1030 . . 3  |-  ( ( F/ x ps  /\  A. x ( th  ->  (
ph 
<->  ps ) )  /\  E. x th )  ->  A. x ( ps  ->  ( th  ->  ph ) ) )
15 19.21t 1986 . . . 4  |-  ( F/ x ps  ->  ( A. x ( ps  ->  ( th  ->  ph ) )  <-> 
( ps  ->  A. x
( th  ->  ph )
) ) )
16153ad2ant1 1029 . . 3  |-  ( ( F/ x ps  /\  A. x ( th  ->  (
ph 
<->  ps ) )  /\  E. x th )  -> 
( A. x ( ps  ->  ( th  ->  ph ) )  <->  ( ps  ->  A. x ( th 
->  ph ) ) ) )
1714, 16mpbid 214 . 2  |-  ( ( F/ x ps  /\  A. x ( th  ->  (
ph 
<->  ps ) )  /\  E. x th )  -> 
( ps  ->  A. x
( th  ->  ph )
) )
189, 17impbid 194 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 188    /\ w3a 985   A.wal 1442   E.wex 1663   F/wnf 1667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-12 1933
This theorem depends on definitions:  df-bi 189  df-an 373  df-3an 987  df-ex 1664  df-nf 1668
This theorem is referenced by:  bj-ceqsalt  31484  bj-ceqsaltv  31485  bj-ceqsalg0  31486
  Copyright terms: Public domain W3C validator