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

Theorem imbi12 28282
Description: Implication form of imbi12i 316. imbi12 28282 is imbi12VD 28649 without virtual deductions and was automatically derived from imbi12VD 28649 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 143 . . 3  |-  ( -.  ( ( ph  <->  ps )  ->  -.  ( ch  <->  th )
)  ->  ( ph  <->  ps ) )
2 simprim 142 . . 3  |-  ( -.  ( ( ph  <->  ps )  ->  -.  ( ch  <->  th )
)  ->  ( ch  <->  th ) )
31, 2imbi12d 311 . 2  |-  ( -.  ( ( ph  <->  ps )  ->  -.  ( ch  <->  th )
)  ->  ( ( ph  ->  ch )  <->  ( ps  ->  th ) ) )
43expi 141 1  |-  ( (
ph 
<->  ps )  ->  (
( ch  <->  th )  ->  ( ( ph  ->  ch )  <->  ( ps  ->  th ) ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176
This theorem is referenced by:  imbi13  28283  imbi13VD  28650  sbcssVD  28659
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 177
  Copyright terms: Public domain W3C validator