Theorem orim12d 979

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

Syntax hints:   → wi 4   ∨ wo 860

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 210  df-an 401  df-or 861

This theorem is referenced by:  orim12da  980  orim1d  981  orim2d  982  3orim123d  1468  preq12b  4811  trun  5223  propeqop  5481  fr2nr  5629  sossfld  6176  ordtri3or  6382  ordelinel  6453  funun  6571  soisores  7315  sorpsscmpl  7721  ordunisuc2  7828  fnse  8117  oaord  8520  omord2  8540  omcan  8542  oeord  8562  oecan  8563  nnaord  8593  nnmord  8606  omsmo  8632  swoer  8714  unxpwdom  9539  rankxplim3  9841  cdainflem  10159  ackbij2  10213  sornom  10249  fin23lem20  10309  fpwwe2lem9  10612  inatsk  10751  ltadd2  11302  ltord1  11728  ltmul1  12056  lt2msq  12091  zle0orge1  12599  mul2lt0bi  13115  xmullem2  13282  difreicc  13502  fzospliti  13711  om2uzlti  13977  om2uzlt2i  13978  om2uzf1oi  13980  absor  15341  ruclem12  16287  dvdslelem  16357  odd2np1lem  16388  odd2np1  16389  isprm6  16763  pythagtrip  16884  pc2dvds  16929  mreexexlem4d  17693  mreexexd  17694  chnccat  18672  ablsimpgprmd  20178  irredrmul  20500  isprmidlc  21434  rhmpreimaprmidl  21439  znidomb  21671  mplsubrglem  22113  ppttop  23125  filconn  24001  trufil  24028  ufildr  24049  plycj  26395  plycjOLD  26397  cosord  26654  logdivlt  26744  isosctrlem2  26942  atans2  27054  wilthlem2  27191  basellem3  27205  lgsdir2lem4  27450  pntpbnd1  27708  nofv  27779  nolesgn2o  27793  noetalem1  27863  om2noseqlt2  28451  om2noseqf1o  28452  zcuts0  28559  mirhl  28910  axcontlem2  29224  axcontlem4  29226  ex-natded5.13-2  30676  hiidge0  31359  chirredlem4  32654  disjxpin  32843  nn0xmulclb  33028  iocinif  33038  pmtrcnelor  33324  minplyirred  34018  erdszelem11  35564  erdsze2lem2  35567  satfv1  35726  satfdmlem  35731  fmla1  35750  satffunlem2lem2  35769  pm3.48ALT  36049  dfon2lem5  36148  btwnconn1lem14  36463  btwnconn2  36465  bj-nnford  37244  poimir  38164  ispridlc  38581  lcvexchlem4  39673  lcvexchlem5  39674  paddss1  40453  paddss2  40454  mulgt0con1dlem  43103  rexzrexnn0  43393  pell14qrdich  43458  acongsym  43565  dvdsacongtr  43573  or3or  44611  clsk1indlem3  44631  mnringmulrcld  44816  grlimprclnbgrvtx  48619  nn0eo  49159  prelrrx2b  49345  itscnhlc0xyqsol  49396  itschlc0xyqsol  49398  inlinecirc02plem  49417