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  1443  preq12b  4855  propeqop  5517  fr2nr  5666  sossfld  6208  ordtri3or  6418  ordelinel  6487  funun  6614  soisores  7347  sorpsscmpl  7753  sucexeloniOLD  7830  suceloniOLD  7832  ordunisuc2  7865  fnse  8157  oaord  8584  omord2  8604  omcan  8606  oeord  8625  oecan  8626  nnaord  8656  nnmord  8669  omsmo  8695  swoer  8775  unxpwdom  9627  rankxplim3  9919  cdainflem  10226  ackbij2  10280  sornom  10315  fin23lem20  10375  fpwwe2lem9  10677  inatsk  10816  ltadd2  11363  ltord1  11787  ltmul1  12115  lt2msq  12151  zle0orge1  12628  mul2lt0bi  13139  xmullem2  13304  difreicc  13521  fzospliti  13728  om2uzlti  13988  om2uzlt2i  13989  om2uzf1oi  13991  absor  15336  ruclem12  16274  dvdslelem  16343  odd2np1lem  16374  odd2np1  16375  isprm6  16748  pythagtrip  16868  pc2dvds  16913  mreexexlem4d  17692  mreexexd  17693  ablsimpgprmd  20150  irredrmul  20444  znidomb  21598  mplsubrglem  22042  ppttop  23030  filconn  23907  trufil  23934  ufildr  23955  plycj  26332  plycjOLD  26334  cosord  26588  logdivlt  26678  isosctrlem2  26877  atans2  26989  wilthlem2  27127  basellem3  27141  lgsdir2lem4  27387  pntpbnd1  27645  nofv  27717  nolesgn2o  27731  noetalem1  27801  om2noseqlt2  28321  om2noseqf1o  28322  mirhl  28702  axcontlem2  28995  axcontlem4  28997  ex-natded5.13-2  30445  hiidge0  31127  chirredlem4  32422  orim12da  32487  disjxpin  32608  nn0xmulclb  32782  iocinif  32790  pmtrcnelor  33094  isprmidlc  33455  rhmpreimaprmidl  33459  minplyirred  33719  erdszelem11  35186  erdsze2lem2  35189  satfv1  35348  satfdmlem  35353  fmla1  35372  satffunlem2lem2  35391  pm3.48ALT  35671  dfon2lem5  35769  btwnconn1lem14  36082  btwnconn2  36084  bj-nnford  36734  poimir  37640  ispridlc  38057  lcvexchlem4  39019  lcvexchlem5  39020  paddss1  39800  paddss2  39801  mulgt0con1dlem  42464  rexzrexnn0  42792  pell14qrdich  42857  acongsym  42965  dvdsacongtr  42973  or3or  44013  clsk1indlem3  44033  mnringmulrcld  44224  nn0eo  48378  prelrrx2b  48564  itscnhlc0xyqsol  48615  itschlc0xyqsol  48617  inlinecirc02plem  48636