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  4806  propeqop  5455  fr2nr  5601  sossfld  6144  ordtri3or  6349  ordelinel  6420  funun  6538  soisores  7273  sorpsscmpl  7679  ordunisuc2  7786  fnse  8075  oaord  8474  omord2  8494  omcan  8496  oeord  8516  oecan  8517  nnaord  8547  nnmord  8560  omsmo  8586  swoer  8666  unxpwdom  9494  rankxplim3  9793  cdainflem  10098  ackbij2  10152  sornom  10187  fin23lem20  10247  fpwwe2lem9  10550  inatsk  10689  ltadd2  11237  ltord1  11663  ltmul1  11991  lt2msq  12027  zle0orge1  12505  mul2lt0bi  13013  xmullem2  13180  difreicc  13400  fzospliti  13607  om2uzlti  13873  om2uzlt2i  13874  om2uzf1oi  13876  absor  15223  ruclem12  16166  dvdslelem  16236  odd2np1lem  16267  odd2np1  16268  isprm6  16641  pythagtrip  16762  pc2dvds  16807  mreexexlem4d  17570  mreexexd  17571  chnccat  18549  ablsimpgprmd  20046  irredrmul  20363  znidomb  21516  mplsubrglem  21959  ppttop  22951  filconn  23827  trufil  23854  ufildr  23875  plycj  26239  plycjOLD  26241  cosord  26496  logdivlt  26586  isosctrlem2  26785  atans2  26897  wilthlem2  27035  basellem3  27049  lgsdir2lem4  27295  pntpbnd1  27553  nofv  27625  nolesgn2o  27639  noetalem1  27709  om2noseqlt2  28296  om2noseqf1o  28297  zcuts0  28404  mirhl  28751  axcontlem2  29038  axcontlem4  29040  ex-natded5.13-2  30491  hiidge0  31173  chirredlem4  32468  orim12da  32532  disjxpin  32663  nn0xmulclb  32851  iocinif  32861  pmtrcnelor  33173  isprmidlc  33528  rhmpreimaprmidl  33532  minplyirred  33868  erdszelem11  35395  erdsze2lem2  35398  satfv1  35557  satfdmlem  35562  fmla1  35581  satffunlem2lem2  35600  pm3.48ALT  35880  dfon2lem5  35979  btwnconn1lem14  36294  btwnconn2  36296  bj-nnford  36952  poimir  37850  ispridlc  38267  lcvexchlem4  39293  lcvexchlem5  39294  paddss1  40073  paddss2  40074  mulgt0con1dlem  42720  rexzrexnn0  43042  pell14qrdich  43107  acongsym  43214  dvdsacongtr  43222  or3or  44260  clsk1indlem3  44280  mnringmulrcld  44465  grlimprclnbgrvtx  48241  nn0eo  48770  prelrrx2b  48956  itscnhlc0xyqsol  49007  itschlc0xyqsol  49009  inlinecirc02plem  49028