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

Theorem pm2.61ian 810
 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 415 . 2 (𝜑 → (𝜓𝜒))
3 pm2.61ian.2 . . 3 ((¬ 𝜑𝜓) → 𝜒)
43ex 415 . 2 𝜑 → (𝜓𝜒))
52, 4pm2.61i 184 1 (𝜓𝜒)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398 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 209  df-an 399 This theorem is referenced by:  4cases  1035  cases2ALT  1043  consensus  1047  preqsnd  4781  csbexg  5205  snopeqop  5387  xpcan2  6027  tfindsg  7567  findsg  7601  ixpexg  8478  fipwss  8885  ranklim  9265  fin23lem14  9747  fzoval  13031  modsumfzodifsn  13304  hashge2el2dif  13830  iswrdi  13857  ffz0iswrdOLD  13884  swrd0  14012  swrdsbslen  14018  swrdspsleq  14019  pfxccatin12  14087  swrdccat  14089  pfxccat3a  14092  repswswrd  14138  cshword  14145  cshwcsh2id  14182  dvdsabseq  15655  m1exp1  15719  flodddiv4  15756  dfgcd2  15886  lcmftp  15972  prmop1  16366  fvprmselelfz  16372  ressbas  16546  resslem  16549  ressinbas  16552  cntzval  18443  symg2bas  18513  sralem  19941  srasca  19945  sravsca  19946  sraip  19947  ocvval  20803  dsmmval  20870  dmatmul  21098  1mavmul  21149  mavmul0g  21154  1marepvmarrepid  21176  smadiadetglem2  21273  1elcpmat  21315  decpmatid  21370  tnglem  23241  tngds  23249  gausslemma2dlem1a  25933  2lgslem1c  25961  2sqreulem1  26014  2sqreunnlem1  26017  clwlkclwwlklem2a4  27767  clwlkclwwlklem2a  27768  clwwisshclwwsn  27786  clwwlknon1nloop  27870  eucrctshift  28014  eucrct2eupth  28016  unopbd  29784  nmopcoi  29864  resvsca  30896  resvlem  30897  satfv1lem  32602  noprefixmo  33195  nosupno  33196  nosupbday  33198  nosupbnd1lem5  33205  nosupbnd1  33207  nosupbnd2  33209  bj-prmoore  34399  ax12indalem  36073  afvres  43362  afvco2  43366  2ffzoeq  43519  ply1mulgsumlem2  44432  lcoel0  44474  lindslinindsimp1  44503  difmodm1lt  44573  digexp  44658  dig1  44659  itsclc0yqsol  44742
 Copyright terms: Public domain W3C validator