Theorem pm2.61ian 824

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  4cases  1056  cases2ALT  1064  consensus  1068  preqsnd  4819  csbexg  5267  snopeqop  5483  xpcan2  6170  tfindsg  7857  findsg  7894  ixpexg  8929  fipwss  9399  ranklim  9826  fin23lem14  10335  fzoval  13715  modsumfzodifsn  14008  hashge2el2dif  14545  iswrdi  14582  swrd0  14728  swrdsbslen  14734  swrdspsleq  14735  pfxccatin12  14802  swrdccat  14804  pfxccat3a  14807  repswswrd  14855  cshword  14862  cshwcsh2id  14899  dvdsabseq  16403  m1exp1  16466  flodddiv4  16505  dfgcd2  16636  lcmftp  16726  prmop1  17130  fvprmselelfz  17136  ressbas  17328  resseqnbas  17334  ressinbas  17337  cntzval  19448  symg2bas  19520  sralem  21360  srasca  21364  sravsca  21365  sraip  21366  isfieldidl  21449  ocvval  21880  dsmmval  21947  dmatmul  22719  1mavmul  22770  mavmul0g  22775  1marepvmarrepid  22797  smadiadetglem2  22894  1elcpmat  22940  decpmatid  22995  tnglem  24866  tngds  24874  gausslemma2dlem1a  27601  2lgslem1c  27629  2sqreulem1  27682  2sqreunnlem1  27685  nosupno  27939  nosupbday  27941  nosupbnd1lem5  27948  nosupbnd1  27950  nosupbnd2  27952  noinfno  27954  noinfbday  27956  noinfbnd1lem5  27963  noinfbnd1  27965  noinfbnd2  27967  madess  28131  abssge0  28510  clwlkclwwlklem2a4  30467  clwlkclwwlklem2a  30468  clwwisshclwwsn  30486  clwwlknon1nloop  30569  eucrctshift  30723  eucrct2eupth  30725  unopbd  32496  nmopcoi  32576  resvsca  33772  resvlem  33773  satfv1lem  35941  bj-prmoore  37865  ax12indalem  39818  afvres  48060  afvco2  48064  2ffzoeq  48216  difmodm1lt  48253  ply1mulgsumlem2  49317  lcoel0  49358  lindslinindsimp1  49387  digexp  49537  dig1  49538  itsclc0yqsol  49694