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 812
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 397 . 2 (𝜑 → (𝜓𝜒))
3 pm2.61ian.2 . . 3 ((¬ 𝜑𝜓) → 𝜒)
43ex 397 . 2 𝜑 → (𝜓𝜒))
52, 4pm2.61i 176 1 (𝜓𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  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 197  df-an 383
This theorem is referenced by:  4cases  1025  cases2ALT  1033  consensus  1039  preqsnd  4523  csbexg  4926  snopeqop  5098  xpcan2  5712  tfindsg  7207  findsg  7240  ixpexg  8086  fipwss  8491  ranklim  8871  fin23lem14  9357  fzoval  12679  modsumfzodifsn  12951  hashge2el2dif  13464  iswrdi  13505  ffz0iswrd  13528  ccat1st1st  13611  swrd0  13643  swrdsbslen  13657  swrdspsleq  13658  swrdccatin12  13700  swrdccat  13702  repswswrd  13740  cshword  13746  cshwcsh2id  13783  dvdsabseq  15244  m1exp1  15301  flodddiv4  15345  dfgcd2  15471  lcmftp  15557  prmop1  15949  fvprmselelfz  15955  ressbas  16137  resslem  16140  ressinbas  16143  cntzval  17961  symg2bas  18025  sralem  19392  srasca  19396  sravsca  19397  sraip  19398  ocvval  20228  dsmmval  20295  dmatmul  20521  1mavmul  20572  mavmul0g  20577  1marepvmarrepid  20599  smadiadetglem2  20697  1elcpmat  20740  decpmatid  20795  tnglem  22664  tngds  22672  gausslemma2dlem1a  25311  2lgslem1c  25339  clwlkclwwlklem2a4  27147  clwlkclwwlklem2a  27148  clwwisshclwwsn  27166  clwwlknon1nloop  27274  eucrctshift  27423  eucrct2eupth  27425  unopbd  29214  nmopcoi  29294  resvsca  30170  resvlem  30171  noprefixmo  32185  nosupno  32186  nosupbday  32188  nosupbnd1lem5  32195  nosupbnd1  32197  nosupbnd2  32199  ax12indalem  34753  afvres  41772  afvco2  41776  2ffzoeq  41866  pfxccatin12  41953  pfxccat3a  41957  cshword2  41965  ply1mulgsumlem2  42703  lcoel0  42745  lindslinindsimp1  42774  difmodm1lt  42845  digexp  42929  dig1  42930
  Copyright terms: Public domain W3C validator