Theorem orim12d 787

Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 10-May-1994.)

Hypotheses

Ref	Expression
orim12d.1	⊢ (𝜑 → (𝜓 → 𝜒))
orim12d.2	⊢ (𝜑 → (𝜃 → 𝜏))

Assertion

Ref	Expression
orim12d	⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))

Proof of Theorem orim12d

Step	Hyp	Ref	Expression
1		orim12d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		orim12d.2	. 2 ⊢ (𝜑 → (𝜃 → 𝜏))
3		pm3.48 786	. 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))

Syntax hints:   → wi 4   ∨ wo 709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1d  788  orim2d  789  3orim123d  1331  19.33b2  1643  eqifdc  3597  preq12b  3801  prel12  3802  exmidsssnc  4237  funun  5303  nnsucelsuc  6558  nnaord  6576  nnmord  6584  swoer  6629  fidceq  6939  fin0or  6956  enomnilem  7213  exmidomni  7217  fodjuomnilemres  7223  ltsopr  7682  cauappcvgprlemloc  7738  caucvgprlemloc  7761  caucvgprprlemloc  7789  suplocexprlemloc  7807  mulextsr1lem  7866  suplocsrlemb  7892  axpre-suploclemres  7987  reapcotr  8644  apcotr  8653  mulext1  8658  mulext  8660  mul0eqap  8716  peano2z  9381  zeo  9450  uzm1  9651  eluzdc  9703  fzospliti  10271  frec2uzltd  10514  absext  11247  qabsor  11259  maxleast  11397  dvdslelemd  12027  odd2np1lem  12056  odd2np1  12057  isprm6  12342  pythagtrip  12479  pc2dvds  12526  ennnfonelemrnh  12660  aprcotr  13919  znidomb  14292  dedekindeulemloc  14941  suplociccreex  14946  dedekindicclemloc  14950  ivthinclemloc  14963  ivthdichlem  14973  plycj  15083  cos11  15175  lgsdir2lem4  15358  uzdcinzz  15530  bj-charfunr  15542  bj-findis  15711  nninfomnilem  15751  isomninnlem  15765