Theorem orim12d 436

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 430	. 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 361	1 |- (ph -> ((ps \/ th) -> (ch \/ ta )))

Syntax hints:   -> wi 2   \/ wo 195

This theorem is referenced by:  orim1d 437  orim2d 438  im3ord 637  preq12b 1874  prel12 1875  ordtri3or 2230  suceloni 2314  funun 2700  oaord 3149  nnmord 3189  nnmcan 3190  omsmo 3196  prlem934b 3932  divge0 4392  om2uzlt 4654  om2uzf1o 4656  hiidge0t 5056

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

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198

metamath.org