Theorem orim12d 967

Description: Disjoin antecedents and consequents in a deduction. See orim12dALT 912 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 966	. 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))

Syntax hints:   → wi 4   ∨ wo 848

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 849

This theorem is referenced by:  orim1d  968  orim2d  969  3orim123d  1447  preq12b  4793  trun  5203  propeqop  5461  fr2nr  5608  sossfld  6150  ordtri3or  6355  ordelinel  6426  funun  6544  soisores  7282  sorpsscmpl  7688  ordunisuc2  7795  fnse  8083  oaord  8482  omord2  8502  omcan  8504  oeord  8524  oecan  8525  nnaord  8555  nnmord  8568  omsmo  8594  swoer  8675  unxpwdom  9504  rankxplim3  9805  cdainflem  10110  ackbij2  10164  sornom  10199  fin23lem20  10259  fpwwe2lem9  10562  inatsk  10701  ltadd2  11250  ltord1  11676  ltmul1  12005  lt2msq  12041  zle0orge1  12541  mul2lt0bi  13050  xmullem2  13217  difreicc  13437  fzospliti  13646  om2uzlti  13912  om2uzlt2i  13913  om2uzf1oi  13915  absor  15262  ruclem12  16208  dvdslelem  16278  odd2np1lem  16309  odd2np1  16310  isprm6  16684  pythagtrip  16805  pc2dvds  16850  mreexexlem4d  17613  mreexexd  17614  chnccat  18592  ablsimpgprmd  20092  irredrmul  20407  znidomb  21541  mplsubrglem  21982  ppttop  22972  filconn  23848  trufil  23875  ufildr  23896  plycj  26242  plycjOLD  26244  cosord  26495  logdivlt  26585  isosctrlem2  26783  atans2  26895  wilthlem2  27032  basellem3  27046  lgsdir2lem4  27291  pntpbnd1  27549  nofv  27621  nolesgn2o  27635  noetalem1  27705  om2noseqlt2  28292  om2noseqf1o  28293  zcuts0  28400  mirhl  28747  axcontlem2  29034  axcontlem4  29036  ex-natded5.13-2  30486  hiidge0  31169  chirredlem4  32464  orim12da  32527  disjxpin  32658  nn0xmulclb  32844  iocinif  32854  pmtrcnelor  33152  isprmidlc  33507  rhmpreimaprmidl  33511  minplyirred  33855  erdszelem11  35383  erdsze2lem2  35386  satfv1  35545  satfdmlem  35550  fmla1  35569  satffunlem2lem2  35588  pm3.48ALT  35868  dfon2lem5  35967  btwnconn1lem14  36282  btwnconn2  36284  bj-nnford  37054  poimir  37974  ispridlc  38391  lcvexchlem4  39483  lcvexchlem5  39484  paddss1  40263  paddss2  40264  mulgt0con1dlem  42914  rexzrexnn0  43232  pell14qrdich  43297  acongsym  43404  dvdsacongtr  43412  or3or  44450  clsk1indlem3  44470  mnringmulrcld  44655  grlimprclnbgrvtx  48475  nn0eo  49004  prelrrx2b  49190  itscnhlc0xyqsol  49241  itschlc0xyqsol  49243  inlinecirc02plem  49262