Theorem orim12d 966

Description: Disjoin antecedents and consequents in a deduction. See orim12dALT 911 for a proof which does not depend on df-an 396. (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 965	. 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))

Syntax hints:   → wi 4   ∨ wo 847

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 207  df-an 396  df-or 848

This theorem is referenced by:  orim1d  967  orim2d  968  3orim123d  1446  preq12b  4801  propeqop  5450  fr2nr  5596  sossfld  6135  ordtri3or  6339  ordelinel  6410  funun  6528  soisores  7264  sorpsscmpl  7670  ordunisuc2  7777  fnse  8066  oaord  8465  omord2  8485  omcan  8487  oeord  8506  oecan  8507  nnaord  8537  nnmord  8550  omsmo  8576  swoer  8656  unxpwdom  9481  rankxplim3  9777  cdainflem  10082  ackbij2  10136  sornom  10171  fin23lem20  10231  fpwwe2lem9  10533  inatsk  10672  ltadd2  11220  ltord1  11646  ltmul1  11974  lt2msq  12010  zle0orge1  12488  mul2lt0bi  13001  xmullem2  13167  difreicc  13387  fzospliti  13594  om2uzlti  13857  om2uzlt2i  13858  om2uzf1oi  13860  absor  15207  ruclem12  16150  dvdslelem  16220  odd2np1lem  16251  odd2np1  16252  isprm6  16625  pythagtrip  16746  pc2dvds  16791  mreexexlem4d  17553  mreexexd  17554  ablsimpgprmd  19996  irredrmul  20312  znidomb  21468  mplsubrglem  21911  ppttop  22892  filconn  23768  trufil  23795  ufildr  23816  plycj  26181  plycjOLD  26183  cosord  26438  logdivlt  26528  isosctrlem2  26727  atans2  26839  wilthlem2  26977  basellem3  26991  lgsdir2lem4  27237  pntpbnd1  27495  nofv  27567  nolesgn2o  27581  noetalem1  27651  om2noseqlt2  28201  om2noseqf1o  28202  mirhl  28628  axcontlem2  28914  axcontlem4  28916  ex-natded5.13-2  30364  hiidge0  31046  chirredlem4  32341  orim12da  32406  disjxpin  32537  nn0xmulclb  32723  iocinif  32733  pmtrcnelor  33042  isprmidlc  33393  rhmpreimaprmidl  33397  minplyirred  33694  erdszelem11  35194  erdsze2lem2  35197  satfv1  35356  satfdmlem  35361  fmla1  35380  satffunlem2lem2  35399  pm3.48ALT  35679  dfon2lem5  35781  btwnconn1lem14  36094  btwnconn2  36096  bj-nnford  36745  poimir  37653  ispridlc  38070  lcvexchlem4  39036  lcvexchlem5  39037  paddss1  39816  paddss2  39817  mulgt0con1dlem  42462  rexzrexnn0  42797  pell14qrdich  42862  acongsym  42969  dvdsacongtr  42977  or3or  44016  clsk1indlem3  44036  mnringmulrcld  44221  grlimprclnbgrvtx  48003  nn0eo  48533  prelrrx2b  48719  itscnhlc0xyqsol  48770  itschlc0xyqsol  48772  inlinecirc02plem  48791