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  8889  apcotr  8898  mulext1  8903  mulext  8905  mul0eqap  8961  peano2z  9630  zeo  9701  uzm1  9903  eluzdc  9960  fzospliti  10534  frec2uzltd  10789  absext  11773  qabsor  11785  maxleast  11923  dvdslelemd  12554  odd2np1lem  12583  odd2np1  12584  isprm6  12869  pythagtrip  13006  pc2dvds  13053  ennnfonelemrnh  13251  aprcotr  14520  znidomb  14918  dedekindeulemloc  15596  suplociccreex  15601  dedekindicclemloc  15605  ivthinclemloc  15618  ivthdichlem  15628  plycj  15738  cos11  15830  lgsdir2lem4  16016  uzdcinzz  16682  bj-charfunr  16692  bj-findis  16861  nninfomnilem  16908  isomninnlem  16926