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  4819  csbexg  5260  snopeqop  5461  xpcan2  6138  tfindsg  7817  findsg  7853  ixpexg  8872  fipwss  9356  ranklim  9773  fin23lem14  10262  fzoval  13597  modsumfzodifsn  13885  hashge2el2dif  14421  iswrdi  14458  swrd0  14599  swrdsbslen  14605  swrdspsleq  14606  pfxccatin12  14674  swrdccat  14676  pfxccat3a  14679  repswswrd  14725  cshword  14732  cshwcsh2id  14770  dvdsabseq  16259  m1exp1  16322  flodddiv4  16361  dfgcd2  16492  lcmftp  16582  prmop1  16985  fvprmselelfz  16991  ressbas  17182  resseqnbas  17188  ressinbas  17191  cntzval  19229  symg2bas  19299  sralem  21059  srasca  21063  sravsca  21064  sraip  21065  ocvval  21552  dsmmval  21619  dmatmul  22360  1mavmul  22411  mavmul0g  22416  1marepvmarrepid  22438  smadiadetglem2  22535  1elcpmat  22578  decpmatid  22633  tnglem  24504  tngds  24512  gausslemma2dlem1a  27252  2lgslem1c  27280  2sqreulem1  27333  2sqreunnlem1  27336  nosupno  27591  nosupbday  27593  nosupbnd1lem5  27600  nosupbnd1  27602  nosupbnd2  27604  noinfno  27606  noinfbday  27608  noinfbnd1lem5  27615  noinfbnd1  27617  noinfbnd2  27619  madess  27764  abssge0  28123  clwlkclwwlklem2a4  29899  clwlkclwwlklem2a  29900  clwwisshclwwsn  29918  clwwlknon1nloop  30001  eucrctshift  30145  eucrct2eupth  30147  unopbd  31917  nmopcoi  31997  resvsca  33277  resvlem  33278  satfv1lem  35322  bj-prmoore  37076  ax12indalem  38911  afvres  47146  afvco2  47150  2ffzoeq  47301  difmodm1lt  47333  ply1mulgsumlem2  48349  lcoel0  48390  lindslinindsimp1  48419  digexp  48569  dig1  48570  itsclc0yqsol  48726