Theorem pm2.61ian 811

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  4883  csbexg  5328  snopeqop  5525  xpcan2  6208  tfindsg  7898  findsg  7937  ixpexg  8980  fipwss  9498  ranklim  9913  fin23lem14  10402  fzoval  13717  modsumfzodifsn  13995  hashge2el2dif  14529  iswrdi  14566  swrd0  14706  swrdsbslen  14712  swrdspsleq  14713  pfxccatin12  14781  swrdccat  14783  pfxccat3a  14786  repswswrd  14832  cshword  14839  cshwcsh2id  14877  dvdsabseq  16361  m1exp1  16424  flodddiv4  16461  dfgcd2  16593  lcmftp  16683  prmop1  17085  fvprmselelfz  17091  ressbas  17293  ressbasOLD  17294  resseqnbas  17300  resslemOLD  17301  ressinbas  17304  cntzval  19361  symg2bas  19434  sralem  21198  sralemOLD  21199  srasca  21206  srascaOLD  21207  sravsca  21208  sravscaOLD  21209  sraip  21210  ocvval  21708  dsmmval  21777  dmatmul  22524  1mavmul  22575  mavmul0g  22580  1marepvmarrepid  22602  smadiadetglem2  22699  1elcpmat  22742  decpmatid  22797  tnglem  24674  tnglemOLD  24675  tngds  24689  tngdsOLD  24690  gausslemma2dlem1a  27427  2lgslem1c  27455  2sqreulem1  27508  2sqreunnlem1  27511  nosupno  27766  nosupbday  27768  nosupbnd1lem5  27775  nosupbnd1  27777  nosupbnd2  27779  noinfno  27781  noinfbday  27783  noinfbnd1lem5  27790  noinfbnd1  27792  noinfbnd2  27794  madess  27933  abssge0  28287  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  clwwisshclwwsn  30048  clwwlknon1nloop  30131  eucrctshift  30275  eucrct2eupth  30277  unopbd  32047  nmopcoi  32127  resvsca  33321  resvlem  33322  resvlemOLD  33323  satfv1lem  35330  bj-prmoore  37081  ax12indalem  38901  afvres  47087  afvco2  47091  2ffzoeq  47242  ply1mulgsumlem2  48116  lcoel0  48157  lindslinindsimp1  48186  difmodm1lt  48256  digexp  48341  dig1  48342  itsclc0yqsol  48498