MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jaodan Structured version   Visualization version   GIF version

Theorem jaodan 821
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
StepHypRef Expression
1 jaodan.1 . . . 4 ((𝜑𝜓) → 𝜒)
21ex 448 . . 3 (𝜑 → (𝜓𝜒))
3 jaodan.2 . . . 4 ((𝜑𝜃) → 𝜒)
43ex 448 . . 3 (𝜑 → (𝜃𝜒))
52, 4jaod 393 . 2 (𝜑 → ((𝜓𝜃) → 𝜒))
65imp 443 1 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 381  wa 382
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 195  df-or 383  df-an 384
This theorem is referenced by:  mpjaodan  822  andi  906  ccase  983  mpjao3dan  1386  relop  5178  poltletr  5430  ordnbtwn  5715  oeoa  7537  oeoe  7539  phplem3  7999  ssnnfi  8037  unwdomg  8345  numwdom  8738  infpssrlem5  8985  fin23lem24  9000  fin23lem28  9018  fin1a2lem10  9087  zornn0g  9183  gchdomtri  9303  fpwwe2lem12  9315  fpwwe2lem13  9316  msqgt0  10393  recextlem2  10503  lemul1a  10722  nnnn0addcl  11166  un0addcl  11169  un0mulcl  11170  elz2  11223  mul2lt0bi  11764  xaddnemnf  11895  xaddnepnf  11896  rexmul  11926  xlemul1a  11943  xrsupsslem  11961  xrinfmsslem  11962  ixxun  12014  fzsplit2  12188  fzsuc2  12219  elfzp12  12239  seqf1olem2  12654  expp1  12680  expneg  12681  expcllem  12684  mulexpz  12713  expaddz  12717  expmulz  12719  faclbnd4lem3  12895  faclbnd4lem4  12896  faclbnd4  12897  bcpasc  12921  ccatass  13166  ccatrn  13167  ccatswrd  13250  cats1un  13269  revccat  13308  summo  14237  sumss2  14246  fsumsplit  14260  geomulcvg  14388  fprodsplit  14477  bpoly2  14569  bpoly3  14570  ef0lem  14590  odd2np1  14845  sadcaddlem  14959  gcdcllem3  15003  dvdslcm  15091  lcmeq0  15093  lcmcl  15094  lcmneg  15096  lcmgcd  15100  rpexp1i  15213  pcid  15357  4sqlem16  15444  funcres2c  16326  lubun  16888  mulgneg  17325  mulgnn0z  17332  frgpup3lem  17955  gsumzunsnd  18120  gsumunsnfd  18121  dprddisj2  18203  dmdprdsplit2  18210  dprdsplit  18212  gsumdixp  18374  lssvs0or  18873  evlslem4  19271  refun0  21066  txhaus  21198  xkoptsub  21205  ptunhmeo  21359  xpsxmetlem  21931  xpsmet  21934  mbfss  23132  itg1addlem2  23183  iblss2  23291  itgsplit  23321  limcres  23369  ftc1lem5  23520  coe1mul3  23576  dgrlt  23739  abelthlem3  23904  atanlogaddlem  24353  atanlogsub  24356  atans2  24371  efrlim  24409  bposlem2  24723  lgsdir2lem4  24766  2sqb  24870  pntpbnd1  24988  ostthlem1  25029  hlbtwn  25220  cgracol  25433  inaghl  25445  brbtwn2  25499  axcontlem2  25559  uvtx01vtx  25782  isoun  28664  nn0sqeq1  28703  eliccelico  28731  elicoelioo  28732  fzsplit3  28742  xrge0iifhom  29113  esumsplit  29244  esumpad2  29247  sibfinima  29530  bnj1137  30119  subfacp1lem4  30221  subfacp1lem5  30222  mclsax  30522  poimirlem2  32380  poimirlem8  32386  poimirlem22  32400  poimirlem28  32406  ftc1cnnc  32453  ftc1anclem2  32455  eqfnun  32485  fdc  32510  incsequz2  32514  unichnidl  32799  lkrss2N  33273  cdlemg27b  34801  tendoex  35080  dihmeetlem2N  35405  dvh3dim3N  35555  rexzrexnn0  36185  pell14qrexpcl  36248  elpell1qr2  36253  acongeq  36367  jm2.23  36380  rpnnen3  36416  radcnvrat  37334  sumpair  38016  cncfiooicclem1  38579  fourierdlem80  38879  fourierdlem93  38892  ccatpfx  40073
  Copyright terms: Public domain W3C validator