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  3639  preq12b  3848  prel12  3849  exmidsssnc  4287  funun  5362  nnsucelsuc  6645  nnaord  6663  nnmord  6671  swoer  6716  fidceq  7039  fin0or  7056  enomnilem  7313  exmidomni  7317  fodjuomnilemres  7323  ltsopr  7791  cauappcvgprlemloc  7847  caucvgprlemloc  7870  caucvgprprlemloc  7898  suplocexprlemloc  7916  mulextsr1lem  7975  suplocsrlemb  8001  axpre-suploclemres  8096  reapcotr  8753  apcotr  8762  mulext1  8767  mulext  8769  mul0eqap  8825  peano2z  9490  zeo  9560  uzm1  9761  eluzdc  9813  fzospliti  10382  frec2uzltd  10633  absext  11582  qabsor  11594  maxleast  11732  dvdslelemd  12362  odd2np1lem  12391  odd2np1  12392  isprm6  12677  pythagtrip  12814  pc2dvds  12861  ennnfonelemrnh  12995  aprcotr  14257  znidomb  14630  dedekindeulemloc  15301  suplociccreex  15306  dedekindicclemloc  15310  ivthinclemloc  15323  ivthdichlem  15333  plycj  15443  cos11  15535  lgsdir2lem4  15718  uzdcinzz  16186  bj-charfunr  16197  bj-findis  16366  fidcen  16379  nninfomnilem  16414  isomninnlem  16428