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

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

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 206  df-an 397

This theorem is referenced by:  4cases  1039  cases2ALT  1047  consensus  1051  preqsnd  4858  csbexg  5309  snopeqop  5505  xpcan2  6173  tfindsg  7846  findsg  7886  ixpexg  8912  fipwss  9420  ranklim  9835  fin23lem14  10324  fzoval  13629  modsumfzodifsn  13905  hashge2el2dif  14437  iswrdi  14464  swrd0  14604  swrdsbslen  14610  swrdspsleq  14611  pfxccatin12  14679  swrdccat  14681  pfxccat3a  14684  repswswrd  14730  cshword  14737  cshwcsh2id  14775  dvdsabseq  16252  m1exp1  16315  flodddiv4  16352  dfgcd2  16484  lcmftp  16569  prmop1  16967  fvprmselelfz  16973  ressbas  17175  ressbasOLD  17176  resseqnbas  17182  resslemOLD  17183  ressinbas  17186  cntzval  19179  symg2bas  19254  sralem  20782  sralemOLD  20783  srasca  20790  srascaOLD  20791  sravsca  20792  sravscaOLD  20793  sraip  20794  ocvval  21211  dsmmval  21280  dmatmul  21990  1mavmul  22041  mavmul0g  22046  1marepvmarrepid  22068  smadiadetglem2  22165  1elcpmat  22208  decpmatid  22263  tnglem  24140  tnglemOLD  24141  tngds  24155  tngdsOLD  24156  gausslemma2dlem1a  26857  2lgslem1c  26885  2sqreulem1  26938  2sqreunnlem1  26941  nosupno  27195  nosupbday  27197  nosupbnd1lem5  27204  nosupbnd1  27206  nosupbnd2  27208  noinfno  27210  noinfbday  27212  noinfbnd1lem5  27219  noinfbnd1  27221  noinfbnd2  27223  madess  27360  clwlkclwwlklem2a4  29239  clwlkclwwlklem2a  29240  clwwisshclwwsn  29258  clwwlknon1nloop  29341  eucrctshift  29485  eucrct2eupth  29487  unopbd  31255  nmopcoi  31335  resvsca  32432  resvlem  32433  resvlemOLD  32434  satfv1lem  34341  bj-prmoore  35984  ax12indalem  37803  afvres  45866  afvco2  45870  2ffzoeq  46022  ply1mulgsumlem2  47021  lcoel0  47062  lindslinindsimp1  47091  difmodm1lt  47161  digexp  47246  dig1  47247  itsclc0yqsol  47403