Theorem orim12d 794

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 793	. 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))

Syntax hints:   → wi 4   ∨ wo 716

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1d  795  orim2d  796  3orim123d  1357  19.33b2  1678  eqifdc  3663  preq12b  3879  prel12  3880  exmidsssnc  4321  funun  5402  nnsucelsuc  6737  nnaord  6755  nnmord  6763  swoer  6808  fidceq  7137  fin0or  7156  fidcen  7169  enomnilem  7442  exmidomni  7446  fodjuomnilemres  7452  ltsopr  7927  cauappcvgprlemloc  7983  caucvgprlemloc  8006  caucvgprprlemloc  8034  suplocexprlemloc  8052  mulextsr1lem  8111  suplocsrlemb  8137  axpre-suploclemres  8232  reapcotr  8890  apcotr  8899  mulext1  8904  mulext  8906  mul0eqap  8964  peano2z  9633  zeo  9704  uzm1  9906  eluzdc  9963  fzospliti  10537  frec2uzltd  10792  absext  11777  qabsor  11789  maxleast  11927  dvdslelemd  12558  odd2np1lem  12587  odd2np1  12588  isprm6  12873  pythagtrip  13010  pc2dvds  13057  ennnfonelemrnh  13255  aprcotr  14539  znidomb  14936  dedekindeulemloc  15614  suplociccreex  15619  dedekindicclemloc  15623  ivthinclemloc  15636  ivthdichlem  15646  plycj  15756  cos11  15848  lgsdir2lem4  16034  uzdcinzz  16710  bj-charfunr  16720  bj-findis  16889  nninfomnilem  16936  isomninnlem  16954