Theorem orim12d 961

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

Syntax hints:   → wi 4   ∨ wo 843

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 209  df-an 399  df-or 844

This theorem is referenced by:  orim1d  962  orim2d  963  3orim123d  1440  preq12b  4781  propeqop  5397  fr2nr  5533  sossfld  6043  ordtri3or  6223  ordelinel  6289  funun  6400  soisores  7080  sorpsscmpl  7460  suceloni  7528  ordunisuc2  7559  fnse  7827  oaord  8173  omord2  8193  omcan  8195  oeord  8214  oecan  8215  nnaord  8245  nnmord  8258  omsmo  8281  swoer  8319  unxpwdom  9053  rankxplim3  9310  cdainflem  9613  ackbij2  9665  sornom  9699  fin23lem20  9759  fpwwe2lem10  10061  inatsk  10200  ltadd2  10744  ltord1  11166  ltmul1  11490  lt2msq  11525  zle0orge1  11999  mul2lt0bi  12496  xmullem2  12659  difreicc  12871  fzospliti  13070  om2uzlti  13319  om2uzlt2i  13320  om2uzf1oi  13322  absor  14660  ruclem12  15594  dvdslelem  15659  odd2np1lem  15689  odd2np1  15690  isprm6  16058  pythagtrip  16171  pc2dvds  16215  mreexexlem4d  16918  mreexexd  16919  ablsimpgprmd  19237  irredrmul  19457  mplsubrglem  20219  znidomb  20708  ppttop  21615  filconn  22491  trufil  22518  ufildr  22539  plycj  24867  cosord  25116  logdivlt  25204  isosctrlem2  25397  atans2  25509  wilthlem2  25646  basellem3  25660  lgsdir2lem4  25904  pntpbnd1  26162  mirhl  26465  axcontlem2  26751  axcontlem4  26753  ex-natded5.13-2  28195  hiidge0  28875  chirredlem4  30170  disjxpin  30338  nn0xmulclb  30496  iocinif  30504  pmtrcnelor  30735  isprmidlc  30963  erdszelem11  32448  erdsze2lem2  32451  satfv1  32610  satfdmlem  32615  fmla1  32634  satffunlem2lem2  32653  dfon2lem5  33032  trpredrec  33077  nofv  33164  nolesgn2o  33178  btwnconn1lem14  33561  btwnconn2  33563  bj-nnford  34080  poimir  34940  ispridlc  35363  lcvexchlem4  36188  lcvexchlem5  36189  paddss1  36968  paddss2  36969  rexzrexnn0  39421  pell14qrdich  39486  acongsym  39593  dvdsacongtr  39601  or3or  40391  clsk1indlem3  40413  nn0eo  44608  prelrrx2b  44721  itscnhlc0xyqsol  44772  itschlc0xyqsol  44774  inlinecirc02plem  44793