Theorem orim12d 791

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

Syntax hints:   → wi 4   ∨ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1d  792  orim2d  793  3orim123d  1354  19.33b2  1675  eqifdc  3640  preq12b  3851  prel12  3852  exmidsssnc  4291  funun  5368  nnsucelsuc  6654  nnaord  6672  nnmord  6680  swoer  6725  fidceq  7051  fin0or  7070  fidcen  7083  enomnilem  7331  exmidomni  7335  fodjuomnilemres  7341  ltsopr  7809  cauappcvgprlemloc  7865  caucvgprlemloc  7888  caucvgprprlemloc  7916  suplocexprlemloc  7934  mulextsr1lem  7993  suplocsrlemb  8019  axpre-suploclemres  8114  reapcotr  8771  apcotr  8780  mulext1  8785  mulext  8787  mul0eqap  8843  peano2z  9508  zeo  9578  uzm1  9780  eluzdc  9837  fzospliti  10406  frec2uzltd  10658  absext  11617  qabsor  11629  maxleast  11767  dvdslelemd  12397  odd2np1lem  12426  odd2np1  12427  isprm6  12712  pythagtrip  12849  pc2dvds  12896  ennnfonelemrnh  13030  aprcotr  14292  znidomb  14665  dedekindeulemloc  15336  suplociccreex  15341  dedekindicclemloc  15345  ivthinclemloc  15358  ivthdichlem  15368  plycj  15478  cos11  15570  lgsdir2lem4  15753  uzdcinzz  16344  bj-charfunr  16355  bj-findis  16524  nninfomnilem  16570  isomninnlem  16584