Theorem orim12d 798

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  orim1d  799  orim2d  800  3orim123d  1361  19.33b2  1682  eqifdc  3677  preq12b  3895  prel12  3896  exmidsssnc  4342  funun  5425  nnsucelsuc  6769  nnaord  6787  nnmord  6795  swoer  6840  fidceq  7177  fin0or  7196  fidcen  7209  enomnilem  7485  exmidomni  7489  fodjuomnilemres  7495  ltsopr  7970  cauappcvgprlemloc  8026  caucvgprlemloc  8049  caucvgprprlemloc  8077  suplocexprlemloc  8095  mulextsr1lem  8154  suplocsrlemb  8180  axpre-suploclemres  8275  reapcotr  8935  apcotr  8944  mulext1  8949  mulext  8951  mul0eqap  9009  peano2z  9690  zeo  9762  uzm1  9969  eluzdc  10026  fzospliti  10602  frec2uzltd  10861  absext  11851  qabsor  11863  maxleast  12002  dvdslelemd  12635  odd2np1lem  12664  odd2np1  12665  isprm6  12951  nn0sqdcq  13013  sqrtrirr  13014  pythagtrip  13091  pc2dvds  13138  ennnfonelemrnh  13365  gsum2d2fi  14274  aprcotr  14706  znidomb  15102  dedekindeulemloc  15878  suplociccreex  15883  dedekindicclemloc  15887  ivthinclemloc  15900  ivthdichlem  15910  plycj  16020  cos11  16114  zprmlogbaplem2  16249  lgsdir2lem4  16388  uzdcinzz  17064  bj-charfunr  17074  bj-findis  17243  nninfomnilem  17300  isomninnlem  17318