Theorem orim12d 565

Description: Disjoin antecedents and consequents in a deduction.

Hypotheses

Ref	Expression
orim12d.1	|- (ph -> (ps -> ch))
orim12d.2	|- (ph -> (th -> ta))

Assertion

Ref	Expression
orim12d	|- (ph -> ((ps \/ th) -> (ch \/ ta)))

Proof of Theorem orim12d

Step	Hyp	Ref	Expression
1		pm3.48 557	. 2 |- (((ps -> ch) /\ (th -> ta)) -> ((ps \/ th) -> (ch \/ ta)))
2		orim12d.1	. 2 |- (ph -> (ps -> ch))
3		orim12d.2	. 2 |- (ph -> (th -> ta))
4	1, 2, 3	sylanc 471	1 |- (ph -> ((ps \/ th) -> (ch \/ ta)))

Syntax hints:   -> wi 3   \/ wo 222

This theorem is referenced by:  orim1d 566  orim2d 567  3orim123d 901  preq12b 2483  prel12 2484  ordtri3or 2979  suceloni 3062  ordunisuc2 3115  funun 3554  oaord 4181  omord2 4198  omcan 4200  oeord 4215  oecan 4216  omsmo 4257  rankxplim3 4714  prlem934b 5138  om2uzlt 6298  om2uzlt2 6299  om2uzf1o 6301  expge0t 6591  expge1t 6593  expcant 6601  expordt 6602  expwordit 6603  expword2it 6605  absort 6865  hiidge0t 8964  irredlem4 10320  cdrci 10494  eqindhome 10541

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 147  df-or 224  df-an 225

Copyright terms: Public domain