Theorem orim12d 961

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

Syntax hints:   → wi 4   ∨ wo 843

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 209  df-an 399  df-or 844

This theorem is referenced by:  orim1d  962  orim2d  963  3orim123d  1440  preq12b  4774  propeqop  5389  fr2nr  5527  sossfld  6037  ordtri3or  6217  ordelinel  6283  funun  6394  soisores  7074  sorpsscmpl  7454  suceloni  7522  ordunisuc2  7553  fnse  7821  oaord  8167  omord2  8187  omcan  8189  oeord  8208  oecan  8209  nnaord  8239  nnmord  8252  omsmo  8275  swoer  8313  unxpwdom  9047  rankxplim3  9304  cdainflem  9607  ackbij2  9659  sornom  9693  fin23lem20  9753  fpwwe2lem10  10055  inatsk  10194  ltadd2  10738  ltord1  11160  ltmul1  11484  lt2msq  11519  zle0orge1  11992  mul2lt0bi  12489  xmullem2  12652  difreicc  12864  fzospliti  13063  om2uzlti  13312  om2uzlt2i  13313  om2uzf1oi  13315  absor  14654  ruclem12  15588  dvdslelem  15653  odd2np1lem  15683  odd2np1  15684  isprm6  16052  pythagtrip  16165  pc2dvds  16209  mreexexlem4d  16912  mreexexd  16913  ablsimpgprmd  19231  irredrmul  19451  mplsubrglem  20213  znidomb  20702  ppttop  21609  filconn  22485  trufil  22512  ufildr  22533  plycj  24861  cosord  25110  logdivlt  25198  isosctrlem2  25391  atans2  25503  wilthlem2  25640  basellem3  25654  lgsdir2lem4  25898  pntpbnd1  26156  mirhl  26459  axcontlem2  26745  axcontlem4  26747  ex-natded5.13-2  28189  hiidge0  28869  chirredlem4  30164  disjxpin  30332  nn0xmulclb  30490  iocinif  30498  pmtrcnelor  30730  isprmidlc  30958  erdszelem11  32443  erdsze2lem2  32446  satfv1  32605  satfdmlem  32610  fmla1  32629  satffunlem2lem2  32648  dfon2lem5  33027  trpredrec  33072  nofv  33159  nolesgn2o  33173  btwnconn1lem14  33556  btwnconn2  33558  bj-nnford  34075  poimir  34919  ispridlc  35342  lcvexchlem4  36167  lcvexchlem5  36168  paddss1  36947  paddss2  36948  rexzrexnn0  39394  pell14qrdich  39459  acongsym  39566  dvdsacongtr  39574  or3or  40364  clsk1indlem3  40386  nn0eo  44582  prelrrx2b  44695  itscnhlc0xyqsol  44746  itschlc0xyqsol  44748  inlinecirc02plem  44767