Theorem jaoian 784

Description: Inference disjoining the antecedents of two implications. (Contributed by NM, 23-Oct-2005.)

Hypotheses

Ref	Expression
jaoian.1
jaoian.2

Assertion

Ref	Expression
jaoian

Proof of Theorem jaoian

Step	Hyp	Ref	Expression
1		jaoian.1	. . . 4
2	1	ex 434	. . 3
3		jaoian.2	. . . 4
4	3	ex 434	. . 3
5	2, 4	jaoi 379	. 2
6	5	imp 429	1

Syntax hints:  ->wi 4  \/wo 368  /\wa 369

This theorem is referenced by:  ccase  946  xaddnemnf  11462  xaddnepnf  11463  faclbnd  12368  faclbnd3  12370  faclbnd4lem1  12371  znf1o  18590  degltlem1  22472  ipasslem3  25748  xrge0iifhom  27919  fzsplit1nn0  30687  tpres  32554

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 185  df-or 370  df-an 371