Theorem idn3 16510

Description: Virtual deduction identity rule for 3 virtual hypotheses.

Assertion

Ref	Expression
idn3	|- . ph, ps, ch   ⊢   ch .

Proof of Theorem idn3

Step	Hyp	Ref	Expression
1		idd 75	. . 3 |- (ps -> (ch -> ch))
2	1	a1i 8	. 2 |- (ph -> (ps -> (ch -> ch)))
3	2	dfvd3ir 16497	1 |- . ph, ps, ch   ⊢   ch .

Syntax hints:   -> wi 3   . vd3 16493

This theorem is referenced by:  suctrALT2VD 16660  en3lplem2VD 16668  exbirVD 16677  exbiriVD 16678  ra4sbc2VD 16679  tratrbVD 16685  ssralv2VD 16690  imbi12VD 16697  imbi13VD 16698  truniALTVD 16702  trintALTVD 16704

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242  df-3an 860  df-vd3 16494

Copyright terms: Public domain