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

Theorem imbi12 28701
Description: Implication form of imbi12i 318. imbi12 28701 is imbi12VD 29083 without virtual deductions and was automatically derived from imbi12VD 29083 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 146 . . 3  |-  ( -.  ( ( ph  <->  ps )  ->  -.  ( ch  <->  th )
)  ->  ( ph  <->  ps ) )
2 simprim 145 . . 3  |-  ( -.  ( ( ph  <->  ps )  ->  -.  ( ch  <->  th )
)  ->  ( ch  <->  th ) )
31, 2imbi12d 313 . 2  |-  ( -.  ( ( ph  <->  ps )  ->  -.  ( ch  <->  th )
)  ->  ( ( ph  ->  ch )  <->  ( ps  ->  th ) ) )
43expi 144 1  |-  ( (
ph 
<->  ps )  ->  (
( ch  <->  th )  ->  ( ( ph  ->  ch )  <->  ( ps  ->  th ) ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178
This theorem is referenced by:  imbi13  28702  imbi13VD  29084  sbcssVD  29093
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator