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 830
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 450 . 2 (𝜑 → (𝜓𝜒))
3 pm2.61ian.2 . . 3 ((¬ 𝜑𝜓) → 𝜒)
43ex 450 . 2 𝜑 → (𝜓𝜒))
52, 4pm2.61i 176 1 (𝜓𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384
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 386
This theorem is referenced by:  4cases  989  cases2  992  consensus  998  sbcrextOLD  3506  csbexg  4783  xpcan2  5559  tfindsg  7045  findsg  7078  ixpexg  7917  fipwss  8320  ranklim  8692  fin23lem14  9140  fzoval  12455  modsumfzodifsn  12726  hashge2el2dif  13245  iswrdi  13292  ffz0iswrd  13315  swrd0  13416  swrdsbslen  13430  swrdspsleq  13431  swrdccatin12  13472  swrdccat  13474  repswswrd  13512  cshword  13518  cshwcsh2id  13555  dvdsabseq  15016  m1exp1  15074  flodddiv4  15118  dfgcd2  15244  lcmftp  15330  prmop1  15723  fvprmselelfz  15729  ressbas  15911  resslem  15914  ressinbas  15917  cntzval  17735  symg2bas  17799  sralem  19158  srasca  19162  sravsca  19163  sraip  19164  ocvval  19992  dsmmval  20059  dmatmul  20284  1mavmul  20335  mavmul0g  20340  1marepvmarrepid  20362  smadiadetglem2  20459  1elcpmat  20501  decpmatid  20556  tnglem  22425  tngds  22433  gausslemma2dlem1a  25071  2lgslem1c  25099  uvtxa01vtx  26279  clwlkclwwlklem2a4  26879  clwlkclwwlklem2a  26880  clwwisshclwwsn  26909  eucrctshift  27083  eucrct2eupth  27085  unopbd  28844  nmopcoi  28924  resvsca  29804  resvlem  29805  noprefixmo  31822  nosupno  31823  nosupbday  31825  nosupbnd1lem5  31832  nosupbnd1  31834  nosupbnd2  31836  ax12indalem  34049  afvres  41015  afvco2  41019  2ffzoeq  41101  pfxccatin12  41190  pfxccat3a  41194  cshword2  41202  ply1mulgsumlem2  41940  lcoel0  41982  lindslinindsimp1  42011  difmodm1lt  42082  digexp  42166  dig1  42167
  Copyright terms: Public domain W3C validator