Theorem jaodan 972

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 418	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		jaodan.2	. . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
4	3	ex 418	. . 3 ⊢ (𝜑 → (𝜃 → 𝜒))
5	2, 4	jaod 873	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
6	5	imp 412	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  mpjaodan  973  andi  1025  ccase  1053  relop  5829  poltletr  6128  ordnbtwn  6461  eqfnun  7041  oeoa  8614  oeoe  8616  ssnnfi  9193  domnsymfi  9223  unwdomg  9585  numwdom  10145  infpssrlem5  10392  fin23lem24  10407  fin23lem28  10425  fin1a2lem10  10494  zornn0g  10590  gchdomtri  10721  fpwwe2lem11  10733  fpwwe2lem12  10734  msqgt0  11843  recextlem2  11954  lemul1a  12178  nnne0  12379  nnnn0addcl  12643  un0addcl  12646  un0mulcl  12647  elz2  12718  mul2lt0bi  13235  xaddnemnf  13373  xaddnepnf  13374  rexmul  13408  xlemul1a  13425  xrsupsslem  13444  xrinfmsslem  13445  ixxun  13499  fzsplit2  13690  fzsuc2  13723  elfzp12  13744  seqf1olem2  14192  expp1  14218  expneg  14219  expcllem  14222  mulexpz  14252  expaddz  14256  expmulz  14258  zzlesq  14357  faclbnd4lem3  14446  faclbnd4lem4  14447  faclbnd4  14448  bcpasc  14472  ccatass  14741  ccatrn  14742  ccatswrd  14826  ccatpfx  14858  cats1un  14878  revccat  14923  summo  15892  sumss2  15901  fsumsplit  15916  geomulcvg  16054  fprodsplit  16142  bpoly2  16232  bpoly3  16233  ef0lem  16253  odd2np1  16520  sadcaddlem  16636  gcdcllem3  16680  dvdslcm  16782  lcmeq0  16784  lcmcl  16785  lcmneg  16787  lcmgcd  16791  rpexp1i  16908  pcid  17060  4sqlem16  17147  funcres2c  18087  lubun  18698  mulgneg  19311  mulgnn0z  19320  frgpup3lem  20000  gsumzunsnd  20179  gsumunsnfd  20180  dprddisj2  20264  dmdprdsplit2  20271  dprdsplit  20273  gsumdixp  20557  lssvs0or  21397  evlslem4  22394  refun0  23843  txhaus  23975  xkoptsub  23982  ptunhmeo  24136  xpsxmetlem  24707  xpsmet  24710  mbfss  25976  itg1addlem2  26027  iblss2  26135  itgsplit  26165  limcres  26215  ftc1lem5  26369  coe1mul3  26426  dgrlt  26594  abelthlem3  26769  atanlogaddlem  27250  atanlogsub  27253  atans2  27268  efrlim  27306  bposlem2  27621  lgsdir2lem4  27664  2sqb  27768  pntpbnd1  27922  ostthlem1  27963  nosepdm  28050  nosupbnd2lem1  28081  negsid  28436  elzn0s  28793  zsbday  28801  zcuts  28802  expsp1  28824  hlbtwn  29086  cgracol  29345  inaghl  29373  brbtwn2  29492  axcontlem2  29552  ifnebib  33196  isoun  33346  eliccelico  33419  elicoelioo  33420  fzsplit3  33435  prodpr  33467  zarclsun  34552  xrge0iifhom  34619  esumsplit  34735  esumpad2  34738  sibfinima  35021  circlemethhgt  35322  bnj1137  35675  subfacp1lem4  36066  subfacp1lem5  36067  mclsax  36452  poimirlem2  38677  poimirlem8  38683  poimirlem22  38697  poimirlem28  38703  ftc1cnnc  38747  ftc1anclem2  38749  dfprop1  38782  fdc  38816  incsequz2  38820  unichnidl  39102  lkrss2N  40363  cdlemg27b  41890  tendoex  42169  dihmeetlem2N  42493  dvh3dim3N  42643  aks6d1c2p2  43306  hashscontpow  43309  aks6d1c5  43326  sticksstones1  43333  sticksstones2  43334  unitscyglem2  43383  ofun  43426  sn-nnne0  43661  nn0addcom  43663  nn0mulcom  43667  zmulcomlem  43668  rexzrexnn0  43948  pell14qrexpcl  44011  elpell1qr2  44016  acongeq  44127  jm2.23  44140  rpnnen3  44176  mnringmulrcld  45363  mnuprdlem3  45395  radcnvrat  45435  sumpair  46188  cncfiooicclem1  47039  fourierdlem80  47332  fourierdlem93  47345  fullthinc  50721  veronesevrowd  51190