Theorem orim12d 775

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

Syntax hints:   → wi 4   ∨ wo 697

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orim1d  776  orim2d  777  3orim123d  1298  19.33b2  1608  eqifdc  3506  preq12b  3697  prel12  3698  exmidsssnc  4126  funun  5167  nnsucelsuc  6387  nnaord  6405  nnmord  6413  swoer  6457  fidceq  6763  fin0or  6780  enomnilem  7010  exmidomni  7014  fodjuomnilemres  7020  ltsopr  7404  cauappcvgprlemloc  7460  caucvgprlemloc  7483  caucvgprprlemloc  7511  suplocexprlemloc  7529  mulextsr1lem  7588  suplocsrlemb  7614  axpre-suploclemres  7709  reapcotr  8360  apcotr  8369  mulext1  8374  mulext  8376  mul0eqap  8431  peano2z  9090  zeo  9156  uzm1  9356  eluzdc  9404  fzospliti  9953  frec2uzltd  10176  absext  10835  qabsor  10847  maxleast  10985  dvdslelemd  11541  odd2np1lem  11569  odd2np1  11570  isprm6  11825  ennnfonelemrnh  11929  dedekindeulemloc  12766  suplociccreex  12771  dedekindicclemloc  12775  ivthinclemloc  12788  uzdcinzz  13005  bj-findis  13177  nninfomnilem  13214  isomninnlem  13225