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

Theorem 3impexpbicomiVD 36894
Description: Virtual deduction proof of 3impexpbicomi 36472. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
h1::  |-  ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) )
qed:1,?: e0a 36799  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
3impexpbicomiVD.1  |-  ( (
ph  /\  ps  /\  ch )  ->  ( th  <->  ta )
)
Assertion
Ref Expression
3impexpbicomiVD  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th )
) ) )

Proof of Theorem 3impexpbicomiVD
StepHypRef Expression
1 3impexpbicomiVD.1 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( th  <->  ta )
)
2 3impexpbicom 36471 . . 3  |-  ( ( ( ph  /\  ps  /\ 
ch )  ->  ( th 
<->  ta ) )  <->  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th )
) ) ) )
32biimpi 197 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  ->  ( th 
<->  ta ) )  -> 
( ph  ->  ( ps 
->  ( ch  ->  ( ta 
<->  th ) ) ) ) )
41, 3e0a 36799 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th )
) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator