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 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  1038  cases2ALT  1046  consensus  1050  preqsnd  4859  csbexg  5310  snopeqop  5506  xpcan2  6176  tfindsg  7854  findsg  7894  ixpexg  8920  fipwss  9428  ranklim  9843  fin23lem14  10332  fzoval  13638  modsumfzodifsn  13914  hashge2el2dif  14446  iswrdi  14473  swrd0  14613  swrdsbslen  14619  swrdspsleq  14620  pfxccatin12  14688  swrdccat  14690  pfxccat3a  14693  repswswrd  14739  cshword  14746  cshwcsh2id  14784  dvdsabseq  16261  m1exp1  16324  flodddiv4  16361  dfgcd2  16493  lcmftp  16578  prmop1  16976  fvprmselelfz  16982  ressbas  17184  ressbasOLD  17185  resseqnbas  17191  resslemOLD  17192  ressinbas  17195  cntzval  19227  symg2bas  19302  sralem  20936  sralemOLD  20937  srasca  20944  srascaOLD  20945  sravsca  20946  sravscaOLD  20947  sraip  20948  ocvval  21440  dsmmval  21509  dmatmul  22220  1mavmul  22271  mavmul0g  22276  1marepvmarrepid  22298  smadiadetglem2  22395  1elcpmat  22438  decpmatid  22493  tnglem  24370  tnglemOLD  24371  tngds  24385  tngdsOLD  24386  gausslemma2dlem1a  27105  2lgslem1c  27133  2sqreulem1  27186  2sqreunnlem1  27189  nosupno  27443  nosupbday  27445  nosupbnd1lem5  27452  nosupbnd1  27454  nosupbnd2  27456  noinfno  27458  noinfbday  27460  noinfbnd1lem5  27467  noinfbnd1  27469  noinfbnd2  27471  madess  27609  clwlkclwwlklem2a4  29518  clwlkclwwlklem2a  29519  clwwisshclwwsn  29537  clwwlknon1nloop  29620  eucrctshift  29764  eucrct2eupth  29766  unopbd  31536  nmopcoi  31616  resvsca  32715  resvlem  32716  resvlemOLD  32717  satfv1lem  34652  bj-prmoore  36300  ax12indalem  38119  afvres  46179  afvco2  46183  2ffzoeq  46335  ply1mulgsumlem2  47156  lcoel0  47197  lindslinindsimp1  47226  difmodm1lt  47296  digexp  47381  dig1  47382  itsclc0yqsol  47538