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

Theorem pm2.61ian 848
Description: Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.)
Hypotheses
Ref Expression
pm2.61ian.1 ((𝜑𝜓) → 𝜒)
pm2.61ian.2 ((¬ 𝜑𝜓) → 𝜒)
Assertion
Ref Expression
pm2.61ian (𝜓𝜒)

Proof of Theorem pm2.61ian
StepHypRef Expression
1 pm2.61ian.1 . . 3 ((𝜑𝜓) → 𝜒)
21ex 449 . 2 (𝜑 → (𝜓𝜒))
3 pm2.61ian.2 . . 3 ((¬ 𝜑𝜓) → 𝜒)
43ex 449 . 2 𝜑 → (𝜓𝜒))
52, 4pm2.61i 176 1 (𝜓𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  4cases  1009  cases2ALT  1017  consensus  1023  sbcrextOLD  3545  csbexg  4825  xpcan2  5606  tfindsg  7102  findsg  7135  ixpexg  7974  fipwss  8376  ranklim  8745  fin23lem14  9193  fzoval  12510  modsumfzodifsn  12783  hashge2el2dif  13300  iswrdi  13341  ffz0iswrd  13364  ccat1st1st  13448  swrd0  13480  swrdsbslen  13494  swrdspsleq  13495  swrdccatin12  13537  swrdccat  13539  repswswrd  13577  cshword  13583  cshwcsh2id  13620  dvdsabseq  15082  m1exp1  15140  flodddiv4  15184  dfgcd2  15310  lcmftp  15396  prmop1  15789  fvprmselelfz  15795  ressbas  15977  resslem  15980  ressinbas  15983  cntzval  17800  symg2bas  17864  sralem  19225  srasca  19229  sravsca  19230  sraip  19231  ocvval  20059  dsmmval  20126  dmatmul  20351  1mavmul  20402  mavmul0g  20407  1marepvmarrepid  20429  smadiadetglem2  20526  1elcpmat  20568  decpmatid  20623  tnglem  22491  tngds  22499  gausslemma2dlem1a  25135  2lgslem1c  25163  clwlkclwwlklem2a4  26963  clwlkclwwlklem2a  26964  clwwisshclwwsn  26973  clwwlknon1nloop  27074  eucrctshift  27221  eucrct2eupth  27223  unopbd  29002  nmopcoi  29082  resvsca  29958  resvlem  29959  noprefixmo  31973  nosupno  31974  nosupbday  31976  nosupbnd1lem5  31983  nosupbnd1  31985  nosupbnd2  31987  ax12indalem  34549  afvres  41573  afvco2  41577  2ffzoeq  41663  pfxccatin12  41750  pfxccat3a  41754  cshword2  41762  ply1mulgsumlem2  42500  lcoel0  42542  lindslinindsimp1  42571  difmodm1lt  42642  digexp  42726  dig1  42727
  Copyright terms: Public domain W3C validator