Theorem 4exbidv 1285

Description: Formula-building rule for 4 existential quantifiers (deduction rule).

Hypothesis

Ref	Expression
4exbidv.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
4exbidv	|- (ph -> (E.xE.yE.zE.wps <-> E.xE.yE.zE.wch))

Distinct variable groups:   ph,x   ph,y   ph,z   ph,w

Proof of Theorem 4exbidv

Step	Hyp	Ref	Expression
1		4exbidv.1	. . 3 |- (ph -> (ps <-> ch))
2	1	2exbidv 1283	. 2 |- (ph -> (E.zE.wps <-> E.zE.wch))
3	2	2exbidv 1283	1 |- (ph -> (E.xE.yE.zE.wps <-> E.xE.yE.zE.wch))

Syntax hints:   -> wi 3   <-> wb 146  E.wex 982

This theorem is referenced by:  copsex4g 2800  opbrop 3244  oprabval3 4036  brecop 4312  th3q 4323  elo 10439  eloi 10630

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983

Copyright terms: Public domain