Theorem orim12d 961

Description: Disjoin antecedents and consequents in a deduction. See orim12dALT 908 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 960	. 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))
4	1, 2, 3	syl2anc 583	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 206  df-an 396  df-or 844

This theorem is referenced by:  orim1d  962  orim2d  963  3orim123d  1442  preq12b  4778  propeqop  5415  fr2nr  5558  sossfld  6078  ordtri3or  6283  ordelinel  6349  funun  6464  soisores  7178  sorpsscmpl  7565  suceloni  7635  ordunisuc2  7666  fnse  7945  oaord  8340  omord2  8360  omcan  8362  oeord  8381  oecan  8382  nnaord  8412  nnmord  8425  omsmo  8448  swoer  8486  unxpwdom  9278  trpredrec  9415  rankxplim3  9570  cdainflem  9874  ackbij2  9930  sornom  9964  fin23lem20  10024  fpwwe2lem9  10326  inatsk  10465  ltadd2  11009  ltord1  11431  ltmul1  11755  lt2msq  11790  zle0orge1  12266  mul2lt0bi  12765  xmullem2  12928  difreicc  13145  fzospliti  13347  om2uzlti  13598  om2uzlt2i  13599  om2uzf1oi  13601  absor  14940  ruclem12  15878  dvdslelem  15946  odd2np1lem  15977  odd2np1  15978  isprm6  16347  pythagtrip  16463  pc2dvds  16508  mreexexlem4d  17273  mreexexd  17274  ablsimpgprmd  19633  irredrmul  19864  znidomb  20681  mplsubrglem  21120  ppttop  22065  filconn  22942  trufil  22969  ufildr  22990  plycj  25343  cosord  25592  logdivlt  25681  isosctrlem2  25874  atans2  25986  wilthlem2  26123  basellem3  26137  lgsdir2lem4  26381  pntpbnd1  26639  mirhl  26944  axcontlem2  27236  axcontlem4  27238  ex-natded5.13-2  28681  hiidge0  29361  chirredlem4  30656  disjxpin  30828  nn0xmulclb  30996  iocinif  31004  pmtrcnelor  31262  isprmidlc  31525  rhmpreimaprmidl  31529  erdszelem11  33063  erdsze2lem2  33066  satfv1  33225  satfdmlem  33230  fmla1  33249  satffunlem2lem2  33268  dfon2lem5  33669  nofv  33787  nolesgn2o  33801  noetalem1  33871  btwnconn1lem14  34329  btwnconn2  34331  bj-nnford  34860  poimir  35737  ispridlc  36155  lcvexchlem4  36978  lcvexchlem5  36979  paddss1  37758  paddss2  37759  mulgt0con1dlem  40348  rexzrexnn0  40542  pell14qrdich  40607  acongsym  40714  dvdsacongtr  40722  or3or  41520  clsk1indlem3  41542  mnringmulrcld  41735  nn0eo  45762  prelrrx2b  45948  itscnhlc0xyqsol  45999  itschlc0xyqsol  46001  inlinecirc02plem  46020