Theorem pm2.61ian 811

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 412	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		pm2.61ian.2	. . 3 ⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜒)
4	3	ex 412	. 2 ⊢ (¬ 𝜑 → (𝜓 → 𝜒))
5	2, 4	pm2.61i 182	1 ⊢ (𝜓 → 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  4cases  1040  cases2ALT  1048  consensus  1052  preqsnd  4815  csbexg  5255  snopeqop  5454  xpcan2  6135  tfindsg  7803  findsg  7839  ixpexg  8860  fipwss  9332  ranklim  9756  fin23lem14  10243  fzoval  13576  modsumfzodifsn  13867  hashge2el2dif  14403  iswrdi  14440  swrd0  14582  swrdsbslen  14588  swrdspsleq  14589  pfxccatin12  14656  swrdccat  14658  pfxccat3a  14661  repswswrd  14707  cshword  14714  cshwcsh2id  14751  dvdsabseq  16240  m1exp1  16303  flodddiv4  16342  dfgcd2  16473  lcmftp  16563  prmop1  16966  fvprmselelfz  16972  ressbas  17163  resseqnbas  17169  ressinbas  17172  cntzval  19250  symg2bas  19322  sralem  21128  srasca  21132  sravsca  21133  sraip  21134  ocvval  21622  dsmmval  21689  dmatmul  22441  1mavmul  22492  mavmul0g  22497  1marepvmarrepid  22519  smadiadetglem2  22616  1elcpmat  22659  decpmatid  22714  tnglem  24584  tngds  24592  gausslemma2dlem1a  27332  2lgslem1c  27360  2sqreulem1  27413  2sqreunnlem1  27416  nosupno  27671  nosupbday  27673  nosupbnd1lem5  27680  nosupbnd1  27682  nosupbnd2  27684  noinfno  27686  noinfbday  27688  noinfbnd1lem5  27695  noinfbnd1  27697  noinfbnd2  27699  madess  27862  abssge0  28241  clwlkclwwlklem2a4  30072  clwlkclwwlklem2a  30073  clwwisshclwwsn  30091  clwwlknon1nloop  30174  eucrctshift  30318  eucrct2eupth  30320  unopbd  32090  nmopcoi  32170  resvsca  33413  resvlem  33414  satfv1lem  35556  bj-prmoore  37320  ax12indalem  39205  afvres  47418  afvco2  47422  2ffzoeq  47573  difmodm1lt  47605  ply1mulgsumlem2  48633  lcoel0  48674  lindslinindsimp1  48703  digexp  48853  dig1  48854  itsclc0yqsol  49010