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  1472  preq12b  4816  trun  5230  propeqop  5492  fr2nr  5640  sossfld  6186  ordtri3or  6395  ordelinel  6466  funun  6584  soisores  7327  sorpsscmpl  7733  ordunisuc2  7841  fnse  8130  oaord  8533  omord2  8553  omcan  8555  oeord  8575  oecan  8576  nnaord  8606  nnmord  8619  omsmo  8645  swoer  8727  unxpwdom  9552  rankxplim3  9854  cdainflem  10172  ackbij2  10226  sornom  10262  fin23lem20  10322  fpwwe2lem9  10625  inatsk  10764  ltadd2  11315  ltord1  11741  ltmul1  12066  lt2msq  12101  zle0orge1  12609  mul2lt0bi  13125  xmullem2  13292  difreicc  13512  fzospliti  13722  om2uzlti  13988  om2uzlt2i  13989  om2uzf1oi  13991  absor  15353  ruclem12  16298  dvdslelem  16368  odd2np1lem  16399  odd2np1  16400  isprm6  16774  pythagtrip  16895  pc2dvds  16940  mreexexlem4d  17704  mreexexd  17705  chnccat  18683  ablsimpgprmd  20188  irredrmul  20510  isprmidlc  21453  rhmpreimaprmidl  21460  znidomb  21692  mplsubrglem  22134  ppttop  23145  filconn  24021  trufil  24048  ufildr  24069  plycj  26415  plycjOLD  26417  cosord  26674  logdivlt  26764  isosctrlem2  26962  atans2  27074  wilthlem2  27211  basellem3  27225  lgsdir2lem4  27470  pntpbnd1  27728  nofv  27799  nolesgn2o  27813  noetalem1  27883  om2noseqlt2  28471  om2noseqf1o  28472  zcuts0  28579  mirhl  28934  axcontlem2  29293  axcontlem4  29295  ex-natded5.13-2  30745  hiidge0  31428  chirredlem4  32723  disjxpin  32911  nn0xmulclb  33094  iocinif  33104  pmtrcnelor  33389  minplyirred  34079  erdszelem11  35671  erdsze2lem2  35674  satfv1  35833  satfdmlem  35838  fmla1  35857  satffunlem2lem2  35876  pm3.48ALT  36156  dfon2lem5  36255  btwnconn1lem14  36570  btwnconn2  36572  bj-nnford  37360  poimir  38282  ispridlc  38699  lcvexchlem4  39789  lcvexchlem5  39790  paddss1  40569  paddss2  40570  mulgt0con1dlem  43221  rexzrexnn0  43511  pell14qrdich  43576  acongsym  43683  dvdsacongtr  43691  or3or  44729  clsk1indlem3  44749  mnringmulrcld  44932  grlimprclnbgrvtx  48741  nn0eo  49285  prelrrx2b  49471  itscnhlc0xyqsol  49522  itschlc0xyqsol  49524  inlinecirc02plem  49543