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

Theorem imbi13 28678
Description: Join three logical equivalences to form equivalence of implications. imbi13 28678 is imbi13VD 29060 without virtual deductions and was automatically derived from imbi13VD 29060 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
imbi13  |-  ( (
ph 
<->  ps )  ->  (
( ch  <->  th )  ->  ( ( ta  <->  et )  ->  ( ( ph  ->  ( ch  ->  ta )
)  <->  ( ps  ->  ( th  ->  et )
) ) ) ) )

Proof of Theorem imbi13
StepHypRef Expression
1 imbi12 28677 . 2  |-  ( ( ch  <->  th )  ->  (
( ta  <->  et )  ->  ( ( ch  ->  ta )  <->  ( th  ->  et ) ) ) )
2 imbi12 28677 . 2  |-  ( (
ph 
<->  ps )  ->  (
( ( ch  ->  ta )  <->  ( th  ->  et ) )  ->  (
( ph  ->  ( ch 
->  ta ) )  <->  ( ps  ->  ( th  ->  et ) ) ) ) )
31, 2syl9r 70 1  |-  ( (
ph 
<->  ps )  ->  (
( ch  <->  th )  ->  ( ( ta  <->  et )  ->  ( ( ph  ->  ( ch  ->  ta )
)  <->  ( ps  ->  ( th  ->  et )
) ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  trsbc  28699  trsbcVD  29063
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