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  1040  cases2ALT  1048  consensus  1052  preqsnd  4863  csbexg  5315  snopeqop  5515  xpcan2  6198  tfindsg  7881  findsg  7919  ixpexg  8960  fipwss  9466  ranklim  9881  fin23lem14  10370  fzoval  13696  modsumfzodifsn  13981  hashge2el2dif  14515  iswrdi  14552  swrd0  14692  swrdsbslen  14698  swrdspsleq  14699  pfxccatin12  14767  swrdccat  14769  pfxccat3a  14772  repswswrd  14818  cshword  14825  cshwcsh2id  14863  dvdsabseq  16346  m1exp1  16409  flodddiv4  16448  dfgcd2  16579  lcmftp  16669  prmop1  17071  fvprmselelfz  17077  ressbas  17279  ressbasOLD  17280  resseqnbas  17286  resslemOLD  17287  ressinbas  17290  cntzval  19351  symg2bas  19424  sralem  21192  sralemOLD  21193  srasca  21200  srascaOLD  21201  sravsca  21202  sravscaOLD  21203  sraip  21204  ocvval  21702  dsmmval  21771  dmatmul  22518  1mavmul  22569  mavmul0g  22574  1marepvmarrepid  22596  smadiadetglem2  22693  1elcpmat  22736  decpmatid  22791  tnglem  24668  tnglemOLD  24669  tngds  24683  tngdsOLD  24684  gausslemma2dlem1a  27423  2lgslem1c  27451  2sqreulem1  27504  2sqreunnlem1  27507  nosupno  27762  nosupbday  27764  nosupbnd1lem5  27771  nosupbnd1  27773  nosupbnd2  27775  noinfno  27777  noinfbday  27779  noinfbnd1lem5  27786  noinfbnd1  27788  noinfbnd2  27790  madess  27929  abssge0  28283  clwlkclwwlklem2a4  30025  clwlkclwwlklem2a  30026  clwwisshclwwsn  30044  clwwlknon1nloop  30127  eucrctshift  30271  eucrct2eupth  30273  unopbd  32043  nmopcoi  32123  resvsca  33335  resvlem  33336  resvlemOLD  33337  satfv1lem  35346  bj-prmoore  37097  ax12indalem  38926  afvres  47121  afvco2  47125  2ffzoeq  47276  ply1mulgsumlem2  48232  lcoel0  48273  lindslinindsimp1  48302  difmodm1lt  48371  digexp  48456  dig1  48457  itsclc0yqsol  48613