Theorem plvofpos 41115

Description: rh is derivable because ONLY one of ch, th, ta, et is implied by mu. (Contributed by Jarvin Udandy, 11-Sep-2020.)

Hypotheses

Ref	Expression
plvofpos.1	|- ( ch <-> ( -. ph /\ -. ps ) )
plvofpos.2	|- ( th <-> ( -. ph /\ ps ) )
plvofpos.3	|- ( ta <-> ( ph /\ -. ps ) )
plvofpos.4	|- ( et <-> ( ph /\ ps ) )
plvofpos.5	|- ( ze <-> ( ( ( ( ( -. ( ( mu -> ch ) /\ ( mu -> th ) ) /\ -. ( ( mu -> ch ) /\ ( mu -> ta ) ) ) /\ -. ( ( mu -> ch ) /\ ( ch -> et ) ) ) /\ -. ( ( mu -> th ) /\ ( mu -> ta ) ) ) /\ -. ( ( mu -> th ) /\ ( mu -> et ) ) ) /\ -. ( ( mu -> ta ) /\ ( mu -> et ) ) ) )
plvofpos.6	|- ( si <-> ( ( ( mu -> ch ) \/ ( mu -> th ) ) \/ ( ( mu -> ta ) \/ ( mu -> et ) ) ) )
plvofpos.7	|- ( rh <-> ( ze /\ si ) )
plvofpos.8	|- ze
plvofpos.9	|- si

Assertion

Ref	Expression
plvofpos	|- rh

Proof of Theorem plvofpos

Step	Hyp	Ref	Expression
1		plvofpos.8	. . 3 |- ze
2		plvofpos.9	. . 3 |- si
3	1, 2	pm3.2i 471	. 2 |- ( ze /\ si )
4		plvofpos.7	. . . 4 |- ( rh <-> ( ze /\ si ) )
5	4	bicomi 214	. . 3 |- ( ( ze /\ si ) <-> rh )
6	5	biimpi 206	. 2 |- ( ( ze /\ si ) -> rh )
7	3, 6	ax-mp 5	1 |- rh

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384

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 197  df-an 386

This theorem is referenced by: (None)