Theorem plvofpos

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

	Ref	Expression
Hypotheses	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	plvofpos	|- rh

Proof

Step	Hyp	Ref	Expression
1		plvofpos.1	|- ( ch <-> ( -. ph /\ -. ps ) )
2		plvofpos.2	|- ( th <-> ( -. ph /\ ps ) )
3		plvofpos.3	|- ( ta <-> ( ph /\ -. ps ) )
4		plvofpos.4	|- ( et <-> ( ph /\ ps ) )
5		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 ) ) ) )
6		plvofpos.6	|- ( si <-> ( ( ( mu -> ch ) \/ ( mu -> th ) ) \/ ( ( mu -> ta ) \/ ( mu -> et ) ) ) )
7		plvofpos.7	|- ( rh <-> ( ze /\ si ) )
8		plvofpos.8	|- ze
9		plvofpos.9	|- si
10	8 9	pm3.2i	|- ( ze /\ si )
11	7	bicomi	|- ( ( ze /\ si ) <-> rh )
12	11	biimpi	|- ( ( ze /\ si ) -> rh )
13	10 12	ax-mp	|- rh