Theorem orim12d 959

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

Syntax hints:   → wi 4   ∨ wo 842

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 208  df-an 397  df-or 843

This theorem is referenced by:  orim1d  960  orim2d  961  3orim123d  1436  preq12b  4688  propeqop  5288  fr2nr  5421  sossfld  5919  ordtri3or  6098  ordelinel  6164  funun  6270  soisores  6943  sorpsscmpl  7318  suceloni  7384  ordunisuc2  7415  fnse  7680  oaord  8023  omord2  8043  omcan  8045  oeord  8064  oecan  8065  nnaord  8095  nnmord  8108  omsmo  8131  swoer  8169  unxpwdom  8899  rankxplim3  9156  cdainflem  9459  ackbij2  9511  sornom  9545  fin23lem20  9605  fpwwe2lem10  9907  inatsk  10046  ltadd2  10591  ltord1  11014  ltmul1  11338  lt2msq  11373  zle0orge1  11846  mul2lt0bi  12345  xmullem2  12508  difreicc  12720  fzospliti  12919  om2uzlti  13168  om2uzlt2i  13169  om2uzf1oi  13171  absor  14494  ruclem12  15427  dvdslelem  15492  odd2np1lem  15522  odd2np1  15523  isprm6  15887  pythagtrip  16000  pc2dvds  16044  mreexexlem4d  16747  mreexexd  16748  irredrmul  19147  mplsubrglem  19907  znidomb  20390  ppttop  21299  filconn  22175  trufil  22202  ufildr  22223  plycj  24550  cosord  24797  logdivlt  24885  isosctrlem2  25078  atans2  25190  wilthlem2  25328  basellem3  25342  lgsdir2lem4  25586  pntpbnd1  25844  mirhl  26147  axcontlem2  26434  axcontlem4  26436  ex-natded5.13-2  27887  hiidge0  28566  chirredlem4  29861  disjxpin  30028  nn0xmulclb  30184  iocinif  30192  pmtrcnelor  30394  erdszelem11  32056  erdsze2lem2  32059  satfv1  32218  satfdmlem  32223  fmla1  32242  satffunlem2lem2  32261  dfon2lem5  32640  trpredrec  32686  nofv  32773  nolesgn2o  32787  btwnconn1lem14  33170  btwnconn2  33172  poimir  34456  ispridlc  34880  lcvexchlem4  35704  lcvexchlem5  35705  paddss1  36484  paddss2  36485  rexzrexnn0  38886  pell14qrdich  38951  acongsym  39058  dvdsacongtr  39066  or3or  39856  clsk1indlem3  39878  ablsimpgprmd  40172  nn0eo  44069  prelrrx2b  44182  itscnhlc0xyqsol  44233  itschlc0xyqsol  44235  inlinecirc02plem  44254