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

Theorem imbi12 28322
Description: Implication form of imbi12i 317. imbi12 28322 is imbi12VD 28703 without virtual deductions and was automatically derived from imbi12VD 28703 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
imbi12  |-  ( (
ph 
<->  ps )  ->  (
( ch  <->  th )  ->  ( ( ph  ->  ch )  <->  ( ps  ->  th ) ) ) )

Proof of Theorem imbi12
StepHypRef Expression
1 simplim 145 . . 3  |-  ( -.  ( ( ph  <->  ps )  ->  -.  ( ch  <->  th )
)  ->  ( ph  <->  ps ) )
2 simprim 144 . . 3  |-  ( -.  ( ( ph  <->  ps )  ->  -.  ( ch  <->  th )
)  ->  ( ch  <->  th ) )
31, 2imbi12d 312 . 2  |-  ( -.  ( ( ph  <->  ps )  ->  -.  ( ch  <->  th )
)  ->  ( ( ph  ->  ch )  <->  ( ps  ->  th ) ) )
43expi 143 1  |-  ( (
ph 
<->  ps )  ->  (
( ch  <->  th )  ->  ( ( ph  ->  ch )  <->  ( ps  ->  th ) ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177
This theorem is referenced by:  imbi13  28323  imbi13VD  28704  sbcssVD  28713
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator