Theorem orim12d 963

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

Syntax hints:   → wi 4   ∨ wo 845

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 397  df-or 846

This theorem is referenced by:  orim1d  964  orim2d  965  3orim123d  1444  preq12b  4813  propeqop  5469  fr2nr  5616  sossfld  6143  ordtri3or  6354  ordelinel  6423  funun  6552  soisores  7277  sorpsscmpl  7676  sucexeloniOLD  7750  suceloniOLD  7752  ordunisuc2  7785  fnse  8070  oaord  8499  omord2  8519  omcan  8521  oeord  8540  oecan  8541  nnaord  8571  nnmord  8584  omsmo  8609  swoer  8685  unxpwdom  9534  rankxplim3  9826  cdainflem  10132  ackbij2  10188  sornom  10222  fin23lem20  10282  fpwwe2lem9  10584  inatsk  10723  ltadd2  11268  ltord1  11690  ltmul1  12014  lt2msq  12049  zle0orge1  12525  mul2lt0bi  13030  xmullem2  13194  difreicc  13411  fzospliti  13614  om2uzlti  13865  om2uzlt2i  13866  om2uzf1oi  13868  absor  15197  ruclem12  16134  dvdslelem  16202  odd2np1lem  16233  odd2np1  16234  isprm6  16601  pythagtrip  16717  pc2dvds  16762  mreexexlem4d  17541  mreexexd  17542  ablsimpgprmd  19908  irredrmul  20152  znidomb  21005  mplsubrglem  21447  ppttop  22394  filconn  23271  trufil  23298  ufildr  23319  plycj  25675  cosord  25924  logdivlt  26013  isosctrlem2  26206  atans2  26318  wilthlem2  26455  basellem3  26469  lgsdir2lem4  26713  pntpbnd1  26971  nofv  27042  nolesgn2o  27056  noetalem1  27126  mirhl  27684  axcontlem2  27977  axcontlem4  27979  ex-natded5.13-2  29423  hiidge0  30103  chirredlem4  31398  disjxpin  31573  nn0xmulclb  31744  iocinif  31752  pmtrcnelor  32012  isprmidlc  32296  rhmpreimaprmidl  32300  erdszelem11  33882  erdsze2lem2  33885  satfv1  34044  satfdmlem  34049  fmla1  34068  satffunlem2lem2  34087  dfon2lem5  34448  btwnconn1lem14  34761  btwnconn2  34763  bj-nnford  35292  poimir  36184  ispridlc  36602  lcvexchlem4  37572  lcvexchlem5  37573  paddss1  38353  paddss2  38354  mulgt0con1dlem  40984  rexzrexnn0  41185  pell14qrdich  41250  acongsym  41358  dvdsacongtr  41366  or3or  42417  clsk1indlem3  42437  mnringmulrcld  42630  nn0eo  46734  prelrrx2b  46920  itscnhlc0xyqsol  46971  itschlc0xyqsol  46973  inlinecirc02plem  46992