Users' Mathboxes Mathbox for Jarvin Udandy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  plvcofphax Structured version   Unicode version

Theorem plvcofphax 38407
Description: Given, a,b,d, and "definitions" for c, e, f, g: g is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.)
Hypotheses
Ref Expression
plvcofphax.1  |-  ( ch  <->  ( ( ( ( ph  /\ 
ps )  <->  ph )  -> 
( ph  /\  -.  ( ph  /\  -.  ph )
) )  /\  ( ph  /\  -.  ( ph  /\ 
-.  ph ) ) ) )
plvcofphax.2  |-  ( ta  <->  ( ( ch  ->  th )  /\  ( ph  <->  ch )  /\  ( ( ph  ->  ps )  ->  ( ps  <->  th ) ) ) )
plvcofphax.3  |-  ( et  <->  ( ch  /\  ta )
)
plvcofphax.4  |-  ph
plvcofphax.5  |-  ps
plvcofphax.6  |-  th
plvcofphax.7  |-  ( ze  <->  -.  ( ps  /\  -.  ta ) )
Assertion
Ref Expression
plvcofphax  |-  ze

Proof of Theorem plvcofphax
StepHypRef Expression
1 plvcofphax.5 . . . . 5  |-  ps
2 plvcofphax.2 . . . . . 6  |-  ( ta  <->  ( ( ch  ->  th )  /\  ( ph  <->  ch )  /\  ( ( ph  ->  ps )  ->  ( ps  <->  th ) ) ) )
3 plvcofphax.4 . . . . . 6  |-  ph
4 plvcofphax.1 . . . . . . 7  |-  ( ch  <->  ( ( ( ( ph  /\ 
ps )  <->  ph )  -> 
( ph  /\  -.  ( ph  /\  -.  ph )
) )  /\  ( ph  /\  -.  ( ph  /\ 
-.  ph ) ) ) )
54, 3, 1plcofph 38404 . . . . . 6  |-  ch
6 plvcofphax.6 . . . . . 6  |-  th
72, 3, 1, 5, 6pldofph 38405 . . . . 5  |-  ta
81, 7pm3.2i 456 . . . 4  |-  ( ps 
/\  ta )
9 pm3.4 563 . . . 4  |-  ( ( ps  /\  ta )  ->  ( ps  ->  ta ) )
108, 9ax-mp 5 . . 3  |-  ( ps 
->  ta )
11 iman 425 . . . 4  |-  ( ( ps  ->  ta )  <->  -.  ( ps  /\  -.  ta ) )
1211biimpi 197 . . 3  |-  ( ( ps  ->  ta )  ->  -.  ( ps  /\  -.  ta ) )
1310, 12ax-mp 5 . 2  |-  -.  ( ps  /\  -.  ta )
14 plvcofphax.7 . . . 4  |-  ( ze  <->  -.  ( ps  /\  -.  ta ) )
1514bicomi 205 . . 3  |-  ( -.  ( ps  /\  -.  ta )  <->  ze )
1615biimpi 197 . 2  |-  ( -.  ( ps  /\  -.  ta )  ->  ze )
1713, 16ax-mp 5 1  |-  ze
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    /\ 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