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

This theorem is referenced by:  4cases  1037  cases2ALT  1045  consensus  1049  preqsnd  4786  csbexg  5229  snopeqop  5414  xpcan2  6069  tfindsg  7682  findsg  7720  ixpexg  8668  fipwss  9118  ranklim  9533  fin23lem14  10020  fzoval  13317  modsumfzodifsn  13592  hashge2el2dif  14122  iswrdi  14149  swrd0  14299  swrdsbslen  14305  swrdspsleq  14306  pfxccatin12  14374  swrdccat  14376  pfxccat3a  14379  repswswrd  14425  cshword  14432  cshwcsh2id  14469  dvdsabseq  15950  m1exp1  16013  flodddiv4  16050  dfgcd2  16182  lcmftp  16269  prmop1  16667  fvprmselelfz  16673  ressbas  16873  ressbasOLD  16874  resseqnbas  16877  resslemOLD  16878  ressinbas  16881  cntzval  18842  symg2bas  18915  sralem  20354  sralemOLD  20355  srasca  20362  sravsca  20363  sraip  20364  ocvval  20784  dsmmval  20851  dmatmul  21554  1mavmul  21605  mavmul0g  21610  1marepvmarrepid  21632  smadiadetglem2  21729  1elcpmat  21772  decpmatid  21827  tnglem  23702  tnglemOLD  23703  tngds  23717  tngdsOLD  23718  gausslemma2dlem1a  26418  2lgslem1c  26446  2sqreulem1  26499  2sqreunnlem1  26502  clwlkclwwlklem2a4  28262  clwlkclwwlklem2a  28263  clwwisshclwwsn  28281  clwwlknon1nloop  28364  eucrctshift  28508  eucrct2eupth  28510  unopbd  30278  nmopcoi  30358  resvsca  31431  resvlem  31432  resvlemOLD  31433  satfv1lem  33224  nosupno  33833  nosupbday  33835  nosupbnd1lem5  33842  nosupbnd1  33844  nosupbnd2  33846  noinfno  33848  noinfbday  33850  noinfbnd1lem5  33857  noinfbnd1  33859  noinfbnd2  33861  madess  33986  bj-prmoore  35213  ax12indalem  36886  afvres  44551  afvco2  44555  2ffzoeq  44708  ply1mulgsumlem2  45616  lcoel0  45657  lindslinindsimp1  45686  difmodm1lt  45756  digexp  45841  dig1  45842  itsclc0yqsol  45998