Theorem orim12d 794

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

Syntax hints:   → wi 4   ∨ wo 716

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1d  795  orim2d  796  3orim123d  1357  19.33b2  1678  eqifdc  3658  preq12b  3873  prel12  3874  exmidsssnc  4315  funun  5396  nnsucelsuc  6723  nnaord  6741  nnmord  6749  swoer  6794  fidceq  7123  fin0or  7142  fidcen  7155  enomnilem  7428  exmidomni  7432  fodjuomnilemres  7438  ltsopr  7910  cauappcvgprlemloc  7966  caucvgprlemloc  7989  caucvgprprlemloc  8017  suplocexprlemloc  8035  mulextsr1lem  8094  suplocsrlemb  8120  axpre-suploclemres  8215  reapcotr  8871  apcotr  8880  mulext1  8885  mulext  8887  mul0eqap  8943  peano2z  9612  zeo  9682  uzm1  9884  eluzdc  9941  fzospliti  10511  frec2uzltd  10764  absext  11744  qabsor  11756  maxleast  11894  dvdslelemd  12525  odd2np1lem  12554  odd2np1  12555  isprm6  12840  pythagtrip  12977  pc2dvds  13024  ennnfonelemrnh  13159  aprcotr  14423  znidomb  14798  dedekindeulemloc  15476  suplociccreex  15481  dedekindicclemloc  15485  ivthinclemloc  15498  ivthdichlem  15508  plycj  15618  cos11  15710  lgsdir2lem4  15896  uzdcinzz  16562  bj-charfunr  16572  bj-findis  16741  nninfomnilem  16788  isomninnlem  16806