Theorem jaodan 956

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 857	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
6	5	imp 407	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396   ∨ 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:  mpjaodan  957  andi  1006  ccase  1036  mpjao3danOLD  1432  axpr  5426  relop  5850  poltletr  6133  ordnbtwn  6457  eqfnun  7038  oeoa  8599  oeoe  8601  ssnnfi  9171  ssnnfiOLD  9172  domnsymfi  9205  phplem3OLD  9221  unwdomg  9581  numwdom  10056  infpssrlem5  10304  fin23lem24  10319  fin23lem28  10337  fin1a2lem10  10406  zornn0g  10502  gchdomtri  10626  fpwwe2lem11  10638  fpwwe2lem12  10639  msqgt0  11738  recextlem2  11849  lemul1a  12072  nnne0  12250  nnnn0addcl  12506  un0addcl  12509  un0mulcl  12510  elz2  12580  mul2lt0bi  13084  xaddnemnf  13219  xaddnepnf  13220  rexmul  13254  xlemul1a  13271  xrsupsslem  13290  xrinfmsslem  13291  ixxun  13344  fzsplit2  13530  fzsuc2  13563  elfzp12  13584  seqf1olem2  14012  expp1  14038  expneg  14039  expcllem  14042  mulexpz  14072  expaddz  14076  expmulz  14078  zzlesq  14174  faclbnd4lem3  14259  faclbnd4lem4  14260  faclbnd4  14261  bcpasc  14285  ccatass  14542  ccatrn  14543  ccatswrd  14622  ccatpfx  14655  cats1un  14675  revccat  14720  summo  15667  sumss2  15676  fsumsplit  15691  geomulcvg  15826  fprodsplit  15914  bpoly2  16005  bpoly3  16006  ef0lem  16026  odd2np1  16288  sadcaddlem  16402  gcdcllem3  16446  dvdslcm  16539  lcmeq0  16541  lcmcl  16542  lcmneg  16544  lcmgcd  16548  rpexp1i  16664  pcid  16810  4sqlem16  16897  funcres2c  17856  lubun  18472  mulgneg  19008  mulgnn0z  19017  frgpup3lem  19686  gsumzunsnd  19865  gsumunsnfd  19866  dprddisj2  19950  dmdprdsplit2  19957  dprdsplit  19959  gsumdixp  20207  lssvs0or  20868  evlslem4  21856  refun0  23239  txhaus  23371  xkoptsub  23378  ptunhmeo  23532  xpsxmetlem  24105  xpsmet  24108  mbfss  25387  itg1addlem2  25438  iblss2  25547  itgsplit  25577  limcres  25627  ftc1lem5  25781  coe1mul3  25841  dgrlt  26004  abelthlem3  26169  atanlogaddlem  26642  atanlogsub  26645  atans2  26660  efrlim  26698  bposlem2  27012  lgsdir2lem4  27055  2sqb  27159  pntpbnd1  27313  ostthlem1  27354  nosepdm  27411  nosupbnd2lem1  27442  negsid  27742  hlbtwn  28117  cgracol  28334  inaghl  28351  brbtwn2  28418  axcontlem2  28478  ifnebib  32036  isoun  32178  eliccelico  32243  elicoelioo  32244  fzsplit3  32260  prodpr  32287  zarclsun  33136  xrge0iifhom  33203  esumsplit  33337  esumpad2  33340  sibfinima  33624  circlemethhgt  33941  bnj1137  34292  subfacp1lem4  34460  subfacp1lem5  34461  mclsax  34846  poimirlem2  36793  poimirlem8  36799  poimirlem22  36813  poimirlem28  36819  ftc1cnnc  36863  ftc1anclem2  36865  fdc  36916  incsequz2  36920  unichnidl  37202  lkrss2N  38342  cdlemg27b  39870  tendoex  40149  dihmeetlem2N  40473  dvh3dim3N  40623  aks6d1c2p2  41263  sticksstones1  41268  sticksstones2  41269  metakunt9  41299  ofun  41364  sn-nnne0  41623  nn0addcom  41625  nn0mulcom  41629  zmulcomlem  41630  rexzrexnn0  41844  pell14qrexpcl  41907  elpell1qr2  41912  acongeq  42024  jm2.23  42037  rpnnen3  42073  mnringmulrcld  43289  mnuprdlem3  43335  radcnvrat  43375  sumpair  44021  cncfiooicclem1  44908  fourierdlem80  45201  fourierdlem93  45214  fullthinc  47754