Theorem orim12d 965

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

Syntax hints:   → wi 4   ∨ wo 847

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 210  df-an 400  df-or 848

This theorem is referenced by:  orim1d  966  orim2d  967  3orim123d  1446  preq12b  4747  propeqop  5375  fr2nr  5514  sossfld  6029  ordtri3or  6223  ordelinel  6289  funun  6404  soisores  7114  sorpsscmpl  7500  suceloni  7570  ordunisuc2  7601  fnse  7878  oaord  8253  omord2  8273  omcan  8275  oeord  8294  oecan  8295  nnaord  8325  nnmord  8338  omsmo  8361  swoer  8399  unxpwdom  9183  trpredrec  9320  rankxplim3  9462  cdainflem  9766  ackbij2  9822  sornom  9856  fin23lem20  9916  fpwwe2lem9  10218  inatsk  10357  ltadd2  10901  ltord1  11323  ltmul1  11647  lt2msq  11682  zle0orge1  12158  mul2lt0bi  12657  xmullem2  12820  difreicc  13037  fzospliti  13239  om2uzlti  13488  om2uzlt2i  13489  om2uzf1oi  13491  absor  14829  ruclem12  15765  dvdslelem  15833  odd2np1lem  15864  odd2np1  15865  isprm6  16234  pythagtrip  16350  pc2dvds  16395  mreexexlem4d  17104  mreexexd  17105  ablsimpgprmd  19456  irredrmul  19679  znidomb  20480  mplsubrglem  20920  ppttop  21858  filconn  22734  trufil  22761  ufildr  22782  plycj  25125  cosord  25374  logdivlt  25463  isosctrlem2  25656  atans2  25768  wilthlem2  25905  basellem3  25919  lgsdir2lem4  26163  pntpbnd1  26421  mirhl  26724  axcontlem2  27010  axcontlem4  27012  ex-natded5.13-2  28453  hiidge0  29133  chirredlem4  30428  disjxpin  30600  nn0xmulclb  30768  iocinif  30776  pmtrcnelor  31033  isprmidlc  31291  rhmpreimaprmidl  31295  erdszelem11  32830  erdsze2lem2  32833  satfv1  32992  satfdmlem  32997  fmla1  33016  satffunlem2lem2  33035  dfon2lem5  33433  nofv  33546  nolesgn2o  33560  noetalem1  33630  btwnconn1lem14  34088  btwnconn2  34090  bj-nnford  34619  poimir  35496  ispridlc  35914  lcvexchlem4  36737  lcvexchlem5  36738  paddss1  37517  paddss2  37518  mulgt0con1dlem  40076  rexzrexnn0  40270  pell14qrdich  40335  acongsym  40442  dvdsacongtr  40450  or3or  41249  clsk1indlem3  41271  mnringmulrcld  41460  nn0eo  45490  prelrrx2b  45676  itscnhlc0xyqsol  45727  itschlc0xyqsol  45729  inlinecirc02plem  45748