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

Theorem lecasei 11324
Description: Ordering elimination by cases. (Contributed by NM, 6-Jul-2007.)
Hypotheses
Ref Expression
lecase.1 (𝜑𝐴 ∈ ℝ)
lecase.2 (𝜑𝐵 ∈ ℝ)
lecase.3 ((𝜑𝐴𝐵) → 𝜓)
lecase.4 ((𝜑𝐵𝐴) → 𝜓)
Assertion
Ref Expression
lecasei (𝜑𝜓)

Proof of Theorem lecasei
StepHypRef Expression
1 lecase.3 . 2 ((𝜑𝐴𝐵) → 𝜓)
2 lecase.4 . 2 ((𝜑𝐵𝐴) → 𝜓)
3 lecase.1 . . 3 (𝜑𝐴 ∈ ℝ)
4 lecase.2 . . 3 (𝜑𝐵 ∈ ℝ)
5 letric 11318 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵𝐵𝐴))
63, 4, 5syl2anc 582 . 2 (𝜑 → (𝐴𝐵𝐵𝐴))
71, 2, 6mpjaodan 955 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wo 843  wcel 2104   class class class wbr 5147  cr 11111  cle 11253
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-resscn 11169  ax-pre-lttri 11186
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258
This theorem is referenced by:  wloglei  11750  nn2ge  12243  max0sub  13179  leabs  15250  max0add  15261  limsupgre  15429  ntrivcvgmul  15852  1arithlem4  16863  mndodcong  19451  metustto  24282  reconn  24564  dyaddisj  25345  volcn  25355  ditgcl  25607  ditgswap  25608  ditgsplit  25610  dvfsumlem3  25780  ftc2ditg  25798  coseq0negpitopi  26249  asinlem3  26612  atanlogaddlem  26654  atanlogadd  26655  ppiub  26943  dchrisum0  27259  pntrmax  27303  padicabv  27369  nacsfix  41752  acongrep  42021  hbt  42174  fzunt1d  42510
  Copyright terms: Public domain W3C validator