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  4813  csbexg  5252  snopeqop  5453  xpcan2  6130  tfindsg  7801  findsg  7837  ixpexg  8856  fipwss  9338  ranklim  9759  fin23lem14  10246  fzoval  13581  modsumfzodifsn  13869  hashge2el2dif  14405  iswrdi  14442  swrd0  14583  swrdsbslen  14589  swrdspsleq  14590  pfxccatin12  14657  swrdccat  14659  pfxccat3a  14662  repswswrd  14708  cshword  14715  cshwcsh2id  14753  dvdsabseq  16242  m1exp1  16305  flodddiv4  16344  dfgcd2  16475  lcmftp  16565  prmop1  16968  fvprmselelfz  16974  ressbas  17165  resseqnbas  17171  ressinbas  17174  cntzval  19218  symg2bas  19290  sralem  21098  srasca  21102  sravsca  21103  sraip  21104  ocvval  21592  dsmmval  21659  dmatmul  22400  1mavmul  22451  mavmul0g  22456  1marepvmarrepid  22478  smadiadetglem2  22575  1elcpmat  22618  decpmatid  22673  tnglem  24544  tngds  24552  gausslemma2dlem1a  27292  2lgslem1c  27320  2sqreulem1  27373  2sqreunnlem1  27376  nosupno  27631  nosupbday  27633  nosupbnd1lem5  27640  nosupbnd1  27642  nosupbnd2  27644  noinfno  27646  noinfbday  27648  noinfbnd1lem5  27655  noinfbnd1  27657  noinfbnd2  27659  madess  27808  abssge0  28170  clwlkclwwlklem2a4  29959  clwlkclwwlklem2a  29960  clwwisshclwwsn  29978  clwwlknon1nloop  30061  eucrctshift  30205  eucrct2eupth  30207  unopbd  31977  nmopcoi  32057  resvsca  33283  resvlem  33284  satfv1lem  35337  bj-prmoore  37091  ax12indalem  38926  afvres  47160  afvco2  47164  2ffzoeq  47315  difmodm1lt  47347  ply1mulgsumlem2  48376  lcoel0  48417  lindslinindsimp1  48446  digexp  48596  dig1  48597  itsclc0yqsol  48753