Theorem mpjaodan 744

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination). (Contributed by Mario Carneiro, 29-May-2016.)

Hypotheses

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

Assertion

Ref	Expression
mpjaodan	⊢ (𝜑 → 𝜒)

Proof of Theorem mpjaodan

Step	Hyp	Ref	Expression
1		jaodan.3	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜃))
2		jaodan.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3		jaodan.2	. . 3 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
4	2, 3	jaodan 743	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)
5	1, 4	mpdan 412	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 102   ∨ wo 661

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  mpjao3dan  1238  ifcldadc  3378  ifeq1dadc  3379  ifcldcd  3381  ordtri2or2exmidlem  4269  reg2exmidlema  4277  nndifsnid  6103  phpm  6351  fidifsnen  6355  fidifsnid  6356  fin0  6369  en2eqpr  6380  fientri3  6381  unsnfidcex  6385  unsnfidcel  6386  mullocprlem  6760  recexprlemloc  6821  z2ge  8893  fztri3or  9058  fzm1  9117  fzneuz  9118  exfzdc  9249  qbtwnzlemstep  9257  rebtwn2zlemstep  9261  modifeq2int  9388  modsumfzodifsn  9398  expaddzaplem  9519  expnbnd  9596  bcval  9676  bccmpl  9681  ibcval5  9690  bcpasc  9693  bccl  9694  resqrexlemnm  9904  resqrexlemcvg  9905  resqrexlemoverl  9907  resqrexlemglsq  9908  leabs  9960  nn0abscl  9971  ltabs  9973  abslt  9974  fzomaxdif  9999  maxleim  10091  maxabslemval  10094  minmax  10112  dvdsle  10244  mod2eq1n2dvds  10279  zsupcllemstep  10341  infssuzex  10345  gcdsupex  10349  gcdsupcl  10350  gcdval  10351  gcddvds  10355  gcdcl  10358  gcd0id  10370  gcdneg  10373  bezoutlemmain  10387  bezoutlemzz  10391  bezoutlemaz  10392  bezoutlembz  10393  dfgcd3  10399  dfgcd2  10403  nn0seqcvgd  10423  eucalgf  10437  eucalginv  10438  dvdslcm  10451  lcmcl  10454  lcmneg  10456  lcmgcd  10460  lcmdvds  10461  lcmid  10462  mulgcddvds  10476  pw2dvdslemn  10543  sqrt2irrap  10558