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

Step	Hyp	Ref	Expression
1		pm2.61ian.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 415	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		pm2.61ian.2	. . 3 ⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜒)
4	3	ex 415	. 2 ⊢ (¬ 𝜑 → (𝜓 → 𝜒))
5	2, 4	pm2.61i 184	1 ⊢ (𝜓 → 𝜒)

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  4783  csbexg  5207  snopeqop  5389  xpcan2  6029  tfindsg  7569  findsg  7603  ixpexg  8480  fipwss  8887  ranklim  9267  fin23lem14  9749  fzoval  13033  modsumfzodifsn  13306  hashge2el2dif  13832  iswrdi  13859  ffz0iswrdOLD  13886  swrd0  14014  swrdsbslen  14020  swrdspsleq  14021  pfxccatin12  14089  swrdccat  14091  pfxccat3a  14094  repswswrd  14140  cshword  14147  cshwcsh2id  14184  dvdsabseq  15657  m1exp1  15721  flodddiv4  15758  dfgcd2  15888  lcmftp  15974  prmop1  16368  fvprmselelfz  16374  ressbas  16548  resslem  16551  ressinbas  16554  cntzval  18445  symg2bas  18515  sralem  19943  srasca  19947  sravsca  19948  sraip  19949  ocvval  20805  dsmmval  20872  dmatmul  21100  1mavmul  21151  mavmul0g  21156  1marepvmarrepid  21178  smadiadetglem2  21275  1elcpmat  21317  decpmatid  21372  tnglem  23243  tngds  23251  gausslemma2dlem1a  25935  2lgslem1c  25963  2sqreulem1  26016  2sqreunnlem1  26019  clwlkclwwlklem2a4  27769  clwlkclwwlklem2a  27770  clwwisshclwwsn  27788  clwwlknon1nloop  27872  eucrctshift  28016  eucrct2eupth  28018  unopbd  29786  nmopcoi  29866  resvsca  30898  resvlem  30899  satfv1lem  32604  noprefixmo  33197  nosupno  33198  nosupbday  33200  nosupbnd1lem5  33207  nosupbnd1  33209  nosupbnd2  33211  bj-prmoore  34401  ax12indalem  36075  afvres  43364  afvco2  43368  2ffzoeq  43521  ply1mulgsumlem2  44434  lcoel0  44476  lindslinindsimp1  44505  difmodm1lt  44575  digexp  44660  dig1  44661  itsclc0yqsol  44744