Theorem pm2.61ian 809

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  1038  cases2ALT  1046  consensus  1050  preqsnd  4789  csbexg  5234  snopeqop  5420  xpcan2  6080  tfindsg  7707  findsg  7746  ixpexg  8710  fipwss  9188  ranklim  9602  fin23lem14  10089  fzoval  13388  modsumfzodifsn  13664  hashge2el2dif  14194  iswrdi  14221  swrd0  14371  swrdsbslen  14377  swrdspsleq  14378  pfxccatin12  14446  swrdccat  14448  pfxccat3a  14451  repswswrd  14497  cshword  14504  cshwcsh2id  14541  dvdsabseq  16022  m1exp1  16085  flodddiv4  16122  dfgcd2  16254  lcmftp  16341  prmop1  16739  fvprmselelfz  16745  ressbas  16947  ressbasOLD  16948  resseqnbas  16951  resslemOLD  16952  ressinbas  16955  cntzval  18927  symg2bas  19000  sralem  20439  sralemOLD  20440  srasca  20447  srascaOLD  20448  sravsca  20449  sravscaOLD  20450  sraip  20451  ocvval  20872  dsmmval  20941  dmatmul  21646  1mavmul  21697  mavmul0g  21702  1marepvmarrepid  21724  smadiadetglem2  21821  1elcpmat  21864  decpmatid  21919  tnglem  23796  tnglemOLD  23797  tngds  23811  tngdsOLD  23812  gausslemma2dlem1a  26513  2lgslem1c  26541  2sqreulem1  26594  2sqreunnlem1  26597  clwlkclwwlklem2a4  28361  clwlkclwwlklem2a  28362  clwwisshclwwsn  28380  clwwlknon1nloop  28463  eucrctshift  28607  eucrct2eupth  28609  unopbd  30377  nmopcoi  30457  resvsca  31529  resvlem  31530  resvlemOLD  31531  satfv1lem  33324  nosupno  33906  nosupbday  33908  nosupbnd1lem5  33915  nosupbnd1  33917  nosupbnd2  33919  noinfno  33921  noinfbday  33923  noinfbnd1lem5  33930  noinfbnd1  33932  noinfbnd2  33934  madess  34059  bj-prmoore  35286  ax12indalem  36959  afvres  44664  afvco2  44668  2ffzoeq  44820  ply1mulgsumlem2  45728  lcoel0  45769  lindslinindsimp1  45798  difmodm1lt  45868  digexp  45953  dig1  45954  itsclc0yqsol  46110