Theorem jaodan 960

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 848

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 207  df-an 396  df-or 849

This theorem is referenced by:  mpjaodan  961  andi  1010  ccase  1038  axprOLD  5431  relop  5861  poltletr  6152  ordnbtwn  6477  eqfnun  7057  oeoa  8635  oeoe  8637  ssnnfi  9209  domnsymfi  9240  phplem3OLD  9256  unwdomg  9624  numwdom  10099  infpssrlem5  10347  fin23lem24  10362  fin23lem28  10380  fin1a2lem10  10449  zornn0g  10545  gchdomtri  10669  fpwwe2lem11  10681  fpwwe2lem12  10682  msqgt0  11783  recextlem2  11894  lemul1a  12121  nnne0  12300  nnnn0addcl  12556  un0addcl  12559  un0mulcl  12560  elz2  12631  mul2lt0bi  13141  xaddnemnf  13278  xaddnepnf  13279  rexmul  13313  xlemul1a  13330  xrsupsslem  13349  xrinfmsslem  13350  ixxun  13403  fzsplit2  13589  fzsuc2  13622  elfzp12  13643  seqf1olem2  14083  expp1  14109  expneg  14110  expcllem  14113  mulexpz  14143  expaddz  14147  expmulz  14149  zzlesq  14245  faclbnd4lem3  14334  faclbnd4lem4  14335  faclbnd4  14336  bcpasc  14360  ccatass  14626  ccatrn  14627  ccatswrd  14706  ccatpfx  14739  cats1un  14759  revccat  14804  summo  15753  sumss2  15762  fsumsplit  15777  geomulcvg  15912  fprodsplit  16002  bpoly2  16093  bpoly3  16094  ef0lem  16114  odd2np1  16378  sadcaddlem  16494  gcdcllem3  16538  dvdslcm  16635  lcmeq0  16637  lcmcl  16638  lcmneg  16640  lcmgcd  16644  rpexp1i  16760  pcid  16911  4sqlem16  16998  funcres2c  17948  lubun  18560  mulgneg  19110  mulgnn0z  19119  frgpup3lem  19795  gsumzunsnd  19974  gsumunsnfd  19975  dprddisj2  20059  dmdprdsplit2  20066  dprdsplit  20068  gsumdixp  20316  lssvs0or  21112  evlslem4  22100  refun0  23523  txhaus  23655  xkoptsub  23662  ptunhmeo  23816  xpsxmetlem  24389  xpsmet  24392  mbfss  25681  itg1addlem2  25732  iblss2  25841  itgsplit  25871  limcres  25921  ftc1lem5  26081  coe1mul3  26138  dgrlt  26306  abelthlem3  26477  atanlogaddlem  26956  atanlogsub  26959  atans2  26974  efrlim  27012  efrlimOLD  27013  bposlem2  27329  lgsdir2lem4  27372  2sqb  27476  pntpbnd1  27630  ostthlem1  27671  nosepdm  27729  nosupbnd2lem1  27760  negsid  28073  elzn0s  28384  zsbday  28392  zscut  28393  expsp1  28412  hlbtwn  28619  cgracol  28836  inaghl  28853  brbtwn2  28920  axcontlem2  28980  ifnebib  32562  isoun  32711  eliccelico  32779  elicoelioo  32780  fzsplit3  32795  prodpr  32828  zarclsun  33869  xrge0iifhom  33936  esumsplit  34054  esumpad2  34057  sibfinima  34341  circlemethhgt  34658  bnj1137  35009  subfacp1lem4  35188  subfacp1lem5  35189  mclsax  35574  poimirlem2  37629  poimirlem8  37635  poimirlem22  37649  poimirlem28  37655  ftc1cnnc  37699  ftc1anclem2  37701  fdc  37752  incsequz2  37756  unichnidl  38038  lkrss2N  39170  cdlemg27b  40698  tendoex  40977  dihmeetlem2N  41301  dvh3dim3N  41451  aks6d1c2p2  42120  hashscontpow  42123  aks6d1c5  42140  sticksstones1  42147  sticksstones2  42148  unitscyglem2  42197  metakunt9  42214  ofun  42277  sn-nnne0  42478  nn0addcom  42480  nn0mulcom  42484  zmulcomlem  42485  rexzrexnn0  42815  pell14qrexpcl  42878  elpell1qr2  42883  acongeq  42995  jm2.23  43008  rpnnen3  43044  mnringmulrcld  44247  mnuprdlem3  44293  radcnvrat  44333  sumpair  45040  cncfiooicclem1  45908  fourierdlem80  46201  fourierdlem93  46214  fullthinc  49099