Theorem pm2.61ian 808

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

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

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 395

This theorem is referenced by:  4cases  1037  cases2ALT  1045  consensus  1049  preqsnd  4858  csbexg  5309  snopeqop  5505  xpcan2  6175  tfindsg  7852  findsg  7892  ixpexg  8918  fipwss  9426  ranklim  9841  fin23lem14  10330  fzoval  13637  modsumfzodifsn  13913  hashge2el2dif  14445  iswrdi  14472  swrd0  14612  swrdsbslen  14618  swrdspsleq  14619  pfxccatin12  14687  swrdccat  14689  pfxccat3a  14692  repswswrd  14738  cshword  14745  cshwcsh2id  14783  dvdsabseq  16260  m1exp1  16323  flodddiv4  16360  dfgcd2  16492  lcmftp  16577  prmop1  16975  fvprmselelfz  16981  ressbas  17183  ressbasOLD  17184  resseqnbas  17190  resslemOLD  17191  ressinbas  17194  cntzval  19226  symg2bas  19301  sralem  20935  sralemOLD  20936  srasca  20943  srascaOLD  20944  sravsca  20945  sravscaOLD  20946  sraip  20947  ocvval  21439  dsmmval  21508  dmatmul  22219  1mavmul  22270  mavmul0g  22275  1marepvmarrepid  22297  smadiadetglem2  22394  1elcpmat  22437  decpmatid  22492  tnglem  24369  tnglemOLD  24370  tngds  24384  tngdsOLD  24385  gausslemma2dlem1a  27104  2lgslem1c  27132  2sqreulem1  27185  2sqreunnlem1  27188  nosupno  27442  nosupbday  27444  nosupbnd1lem5  27451  nosupbnd1  27453  nosupbnd2  27455  noinfno  27457  noinfbday  27459  noinfbnd1lem5  27466  noinfbnd1  27468  noinfbnd2  27470  madess  27608  clwlkclwwlklem2a4  29517  clwlkclwwlklem2a  29518  clwwisshclwwsn  29536  clwwlknon1nloop  29619  eucrctshift  29763  eucrct2eupth  29765  unopbd  31535  nmopcoi  31615  resvsca  32714  resvlem  32715  resvlemOLD  32716  satfv1lem  34651  bj-prmoore  36299  ax12indalem  38118  afvres  46178  afvco2  46182  2ffzoeq  46334  ply1mulgsumlem2  47155  lcoel0  47196  lindslinindsimp1  47225  difmodm1lt  47295  digexp  47380  dig1  47381  itsclc0yqsol  47537