Theorem pm2.61ian 812

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  1041  cases2ALT  1049  consensus  1053  preqsnd  4859  csbexg  5310  snopeqop  5511  xpcan2  6197  tfindsg  7882  findsg  7919  ixpexg  8962  fipwss  9469  ranklim  9884  fin23lem14  10373  fzoval  13700  modsumfzodifsn  13985  hashge2el2dif  14519  iswrdi  14556  swrd0  14696  swrdsbslen  14702  swrdspsleq  14703  pfxccatin12  14771  swrdccat  14773  pfxccat3a  14776  repswswrd  14822  cshword  14829  cshwcsh2id  14867  dvdsabseq  16350  m1exp1  16413  flodddiv4  16452  dfgcd2  16583  lcmftp  16673  prmop1  17076  fvprmselelfz  17082  ressbas  17280  ressbasOLD  17281  resseqnbas  17287  resslemOLD  17288  ressinbas  17291  cntzval  19339  symg2bas  19410  sralem  21175  sralemOLD  21176  srasca  21183  srascaOLD  21184  sravsca  21185  sravscaOLD  21186  sraip  21187  ocvval  21685  dsmmval  21754  dmatmul  22503  1mavmul  22554  mavmul0g  22559  1marepvmarrepid  22581  smadiadetglem2  22678  1elcpmat  22721  decpmatid  22776  tnglem  24653  tnglemOLD  24654  tngds  24668  tngdsOLD  24669  gausslemma2dlem1a  27409  2lgslem1c  27437  2sqreulem1  27490  2sqreunnlem1  27493  nosupno  27748  nosupbday  27750  nosupbnd1lem5  27757  nosupbnd1  27759  nosupbnd2  27761  noinfno  27763  noinfbday  27765  noinfbnd1lem5  27772  noinfbnd1  27774  noinfbnd2  27776  madess  27915  abssge0  28269  clwlkclwwlklem2a4  30016  clwlkclwwlklem2a  30017  clwwisshclwwsn  30035  clwwlknon1nloop  30118  eucrctshift  30262  eucrct2eupth  30264  unopbd  32034  nmopcoi  32114  resvsca  33356  resvlem  33357  resvlemOLD  33358  satfv1lem  35367  bj-prmoore  37116  ax12indalem  38946  afvres  47184  afvco2  47188  2ffzoeq  47339  ply1mulgsumlem2  48304  lcoel0  48345  lindslinindsimp1  48374  difmodm1lt  48443  digexp  48528  dig1  48529  itsclc0yqsol  48685