Theorem orim12d 901

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

Syntax hints:   → wi 4   ∨ wo 382

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385

This theorem is referenced by:  orim1d  902  orim2d  903  3orim123d  1447  preq12b  4413  prel12  4414  propeqop  4999  fr2nr  5121  sossfld  5615  ordtri3or  5793  ordelinel  5863  funun  5970  soisores  6617  sorpsscmpl  6990  suceloni  7055  ordunisuc2  7086  fnse  7339  oaord  7672  omord2  7692  omcan  7694  oeord  7713  oecan  7714  nnaord  7744  nnmord  7757  omsmo  7779  swoer  7817  unxpwdom  8535  rankxplim3  8782  cdainflem  9051  ackbij2  9103  sornom  9137  fin23lem20  9197  fpwwe2lem10  9499  inatsk  9638  ltadd2  10179  ltord1  10592  ltmul1  10911  lt2msq  10946  mul2lt0bi  11974  xmullem2  12133  difreicc  12342  fzospliti  12539  om2uzlti  12789  om2uzlt2i  12790  om2uzf1oi  12792  absor  14084  ruclem12  15014  dvdslelem  15078  odd2np1lem  15111  odd2np1  15112  isprm6  15473  pythagtrip  15586  pc2dvds  15630  mreexexlem4d  16354  mreexexd  16355  mreexexdOLD  16356  irredrmul  18753  mplsubrglem  19487  znidomb  19958  ppttop  20859  filconn  21734  trufil  21761  ufildr  21782  plycj  24078  cosord  24323  logdivlt  24412  isosctrlem2  24594  atans2  24703  wilthlem2  24840  basellem3  24854  lgsdir2lem4  25098  pntpbnd1  25320  mirhl  25619  axcontlem2  25890  axcontlem4  25892  ex-natded5.13-2  27403  hiidge0  28083  chirredlem4  29380  disjxpin  29527  iocinif  29671  erdszelem11  31309  erdsze2lem2  31312  dfon2lem5  31816  trpredrec  31862  nofv  31935  nolesgn2o  31949  btwnconn1lem14  32332  btwnconn2  32334  poimir  33572  ispridlc  33999  lcvexchlem4  34642  lcvexchlem5  34643  paddss1  35421  paddss2  35422  rexzrexnn0  37685  pell14qrdich  37750  acongsym  37860  dvdsacongtr  37868  or3or  38636  clsk1indlem3  38658  nn0eo  42647