Theorem jaodan 955

Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.)

Hypotheses

Ref	Expression
jaodan.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
jaodan.2	⊢ ((𝜑 ∧ 𝜃) → 𝜒)

Assertion

Ref	Expression
jaodan	⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)

Proof of Theorem jaodan

Step	Hyp	Ref	Expression
1		jaodan.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 413	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		jaodan.2	. . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
4	3	ex 413	. . 3 ⊢ (𝜑 → (𝜃 → 𝜒))
5	2, 4	jaod 856	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
6	5	imp 407	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396   ∨ wo 844

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 845

This theorem is referenced by:  mpjaodan  956  andi  1005  ccase  1035  mpjao3danOLD  1431  axpr  5352  relop  5762  poltletr  6042  ordnbtwn  6360  oeoa  8437  oeoe  8439  ssnnfi  8961  ssnnfiOLD  8962  domnsymfi  8995  phplem3OLD  9011  unwdomg  9352  numwdom  9824  infpssrlem5  10072  fin23lem24  10087  fin23lem28  10105  fin1a2lem10  10174  zornn0g  10270  gchdomtri  10394  fpwwe2lem11  10406  fpwwe2lem12  10407  msqgt0  11504  recextlem2  11615  lemul1a  11838  nnnn0addcl  12272  un0addcl  12275  un0mulcl  12276  elz2  12346  mul2lt0bi  12845  xaddnemnf  12979  xaddnepnf  12980  rexmul  13014  xlemul1a  13031  xrsupsslem  13050  xrinfmsslem  13051  ixxun  13104  fzsplit2  13290  fzsuc2  13323  elfzp12  13344  seqf1olem2  13772  expp1  13798  expneg  13799  expcllem  13802  mulexpz  13832  expaddz  13836  expmulz  13838  faclbnd4lem3  14018  faclbnd4lem4  14019  faclbnd4  14020  bcpasc  14044  ccatass  14302  ccatrn  14303  ccatswrd  14390  ccatpfx  14423  cats1un  14443  revccat  14488  summo  15438  sumss2  15447  fsumsplit  15462  geomulcvg  15597  fprodsplit  15685  bpoly2  15776  bpoly3  15777  ef0lem  15797  odd2np1  16059  sadcaddlem  16173  gcdcllem3  16217  dvdslcm  16312  lcmeq0  16314  lcmcl  16315  lcmneg  16317  lcmgcd  16321  rpexp1i  16437  pcid  16583  4sqlem16  16670  funcres2c  17626  lubun  18242  mulgneg  18731  mulgnn0z  18739  frgpup3lem  19392  gsumzunsnd  19566  gsumunsnfd  19567  dprddisj2  19651  dmdprdsplit2  19658  dprdsplit  19660  gsumdixp  19857  lssvs0or  20381  evlslem4  21293  refun0  22675  txhaus  22807  xkoptsub  22814  ptunhmeo  22968  xpsxmetlem  23541  xpsmet  23544  mbfss  24819  itg1addlem2  24870  iblss2  24979  itgsplit  25009  limcres  25059  ftc1lem5  25213  coe1mul3  25273  dgrlt  25436  abelthlem3  25601  atanlogaddlem  26072  atanlogsub  26075  atans2  26090  efrlim  26128  bposlem2  26442  lgsdir2lem4  26485  2sqb  26589  pntpbnd1  26743  ostthlem1  26784  hlbtwn  26981  cgracol  27198  inaghl  27215  brbtwn2  27282  axcontlem2  27342  isoun  31043  eliccelico  31107  elicoelioo  31108  fzsplit3  31124  prodpr  31149  zarclsun  31829  xrge0iifhom  31896  esumsplit  32030  esumpad2  32033  sibfinima  32315  circlemethhgt  32632  bnj1137  32984  subfacp1lem4  33154  subfacp1lem5  33155  mclsax  33540  nosepdm  33896  nosupbnd2lem1  33927  poimirlem2  35788  poimirlem8  35794  poimirlem22  35808  poimirlem28  35814  ftc1cnnc  35858  ftc1anclem2  35860  eqfnun  35889  fdc  35912  incsequz2  35916  unichnidl  36198  lkrss2N  37190  cdlemg27b  38717  tendoex  38996  dihmeetlem2N  39320  dvh3dim3N  39470  sticksstones1  40109  sticksstones2  40110  metakunt9  40140  ofun  40218  rexzrexnn0  40633  pell14qrexpcl  40696  elpell1qr2  40701  acongeq  40812  jm2.23  40825  rpnnen3  40861  mnringmulrcld  41853  mnuprdlem3  41899  radcnvrat  41939  sumpair  42585  cncfiooicclem1  43441  fourierdlem80  43734  fourierdlem93  43747  fullthinc  46338