Theorem orim12d 988

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

Syntax hints:   → wi 4   ∨ wo 874

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 199  df-an 386  df-or 875

This theorem is referenced by:  orim1d  989  orim2d  990  3orim123d  1569  preq12b  4567  prel12OLD  4568  propeqop  5163  fr2nr  5290  sossfld  5797  ordtri3or  5973  ordelinel  6039  funun  6146  soisores  6805  sorpsscmpl  7182  suceloni  7247  ordunisuc2  7278  fnse  7531  oaord  7867  omord2  7887  omcan  7889  oeord  7908  oecan  7909  nnaord  7939  nnmord  7952  omsmo  7974  swoer  8012  unxpwdom  8736  rankxplim3  8994  cdainflem  9301  ackbij2  9353  sornom  9387  fin23lem20  9447  fpwwe2lem10  9749  inatsk  9888  ltadd2  10431  ltord1  10846  ltmul1  11165  lt2msq  11200  mul2lt0bi  12181  xmullem2  12344  difreicc  12558  fzospliti  12755  om2uzlti  13004  om2uzlt2i  13005  om2uzf1oi  13007  absor  14381  ruclem12  15306  dvdslelem  15370  odd2np1lem  15400  odd2np1  15401  isprm6  15759  pythagtrip  15872  pc2dvds  15916  mreexexlem4d  16622  mreexexd  16623  irredrmul  19023  mplsubrglem  19762  znidomb  20231  ppttop  21140  filconn  22015  trufil  22042  ufildr  22063  plycj  24374  cosord  24620  logdivlt  24708  isosctrlem2  24901  atans2  25010  wilthlem2  25147  basellem3  25161  lgsdir2lem4  25405  pntpbnd1  25627  mirhl  25930  axcontlem2  26202  axcontlem4  26204  ex-natded5.13-2  27801  hiidge0  28480  chirredlem4  29777  disjxpin  29918  iocinif  30061  erdszelem11  31700  erdsze2lem2  31703  dfon2lem5  32204  trpredrec  32250  nofv  32323  nolesgn2o  32337  btwnconn1lem14  32720  btwnconn2  32722  poimir  33931  ispridlc  34356  lcvexchlem4  35058  lcvexchlem5  35059  paddss1  35838  paddss2  35839  rexzrexnn0  38154  pell14qrdich  38219  acongsym  38328  dvdsacongtr  38336  or3or  39101  clsk1indlem3  39123  nn0eo  43121