Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sbcim2g Unicode version

Theorem sbcim2g 28601
Description: Distribution of class substitution over a left-nested implication. Similar to sbcimg 3045. sbcim2g 28601 is sbcim2gVD 28967 without virtual deductions and was automatically derived from sbcim2gVD 28967 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
sbcim2g  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  <-> 
( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ) )

Proof of Theorem sbcim2g
StepHypRef Expression
1 sbcimg 3045 . . . 4  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  <-> 
( [. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch ) ) ) )
21biimpd 198 . . 3  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  ->  ( [. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch )
) ) )
3 sbcimg 3045 . . 3  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( ps  ->  ch ) 
<->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch )
) )
4 imbi2 314 . . . 4  |-  ( (
[. A  /  x ]. ( ps  ->  ch ) 
<->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch )
)  ->  ( ( [. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch ) )  <->  ( [. A  /  x ]. ph  ->  (
[. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ) )
54biimpcd 215 . . 3  |-  ( (
[. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch ) )  ->  (
( [. A  /  x ]. ( ps  ->  ch ) 
<->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch )
)  ->  ( [. A  /  x ]. ph  ->  (
[. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ) )
62, 3, 5ee21 1365 . 2  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  ->  ( [. A  /  x ]. ph  ->  (
[. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ) )
7 idd 21 . . . 4  |-  ( A  e.  V  ->  (
( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) )  -> 
( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ) )
8 bi2 189 . . . 4  |-  ( (
[. A  /  x ]. ( ps  ->  ch ) 
<->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch )
)  ->  ( ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch )  ->  [. A  /  x ]. ( ps  ->  ch ) ) )
93, 7, 8ee13 28564 . . 3  |-  ( A  e.  V  ->  (
( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) )  -> 
( [. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch ) ) ) )
109, 1sylibrd 225 . 2  |-  ( A  e.  V  ->  (
( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) )  ->  [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) ) ) )
116, 10impbid 183 1  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  <-> 
( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    e. wcel 1696   [.wsbc 3004
This theorem is referenced by:  trsbc  28603  trsbcVD  28969
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-sbc 3005
  Copyright terms: Public domain W3C validator