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  1640  eqifdc  3584  preq12b  3785  prel12  3786  exmidsssnc  4218  funun  5275  nnsucelsuc  6510  nnaord  6528  nnmord  6536  swoer  6581  fidceq  6887  fin0or  6904  enomnilem  7154  exmidomni  7158  fodjuomnilemres  7164  ltsopr  7613  cauappcvgprlemloc  7669  caucvgprlemloc  7692  caucvgprprlemloc  7720  suplocexprlemloc  7738  mulextsr1lem  7797  suplocsrlemb  7823  axpre-suploclemres  7918  reapcotr  8573  apcotr  8582  mulext1  8587  mulext  8589  mul0eqap  8645  peano2z  9307  zeo  9376  uzm1  9576  eluzdc  9628  fzospliti  10194  frec2uzltd  10421  absext  11090  qabsor  11102  maxleast  11240  dvdslelemd  11867  odd2np1lem  11895  odd2np1  11896  isprm6  12165  pythagtrip  12301  pc2dvds  12347  ennnfonelemrnh  12435  aprcotr  13562  dedekindeulemloc  14494  suplociccreex  14499  dedekindicclemloc  14503  ivthinclemloc  14516  cos11  14671  lgsdir2lem4  14829  uzdcinzz  14947  bj-charfunr  14959  bj-findis  15128  nninfomnilem  15165  isomninnlem  15176