Theorem pm2.61ian 810

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 413	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		pm2.61ian.2	. . 3 ⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜒)
4	3	ex 413	. 2 ⊢ (¬ 𝜑 → (𝜓 → 𝜒))
5	2, 4	pm2.61i 182	1 ⊢ (𝜓 → 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  4cases  1039  cases2ALT  1047  consensus  1051  preqsnd  4859  csbexg  5310  snopeqop  5506  xpcan2  6176  tfindsg  7849  findsg  7889  ixpexg  8915  fipwss  9423  ranklim  9838  fin23lem14  10327  fzoval  13632  modsumfzodifsn  13908  hashge2el2dif  14440  iswrdi  14467  swrd0  14607  swrdsbslen  14613  swrdspsleq  14614  pfxccatin12  14682  swrdccat  14684  pfxccat3a  14687  repswswrd  14733  cshword  14740  cshwcsh2id  14778  dvdsabseq  16255  m1exp1  16318  flodddiv4  16355  dfgcd2  16487  lcmftp  16572  prmop1  16970  fvprmselelfz  16976  ressbas  17178  ressbasOLD  17179  resseqnbas  17185  resslemOLD  17186  ressinbas  17189  cntzval  19184  symg2bas  19259  sralem  20789  sralemOLD  20790  srasca  20797  srascaOLD  20798  sravsca  20799  sravscaOLD  20800  sraip  20801  ocvval  21219  dsmmval  21288  dmatmul  21998  1mavmul  22049  mavmul0g  22054  1marepvmarrepid  22076  smadiadetglem2  22173  1elcpmat  22216  decpmatid  22271  tnglem  24148  tnglemOLD  24149  tngds  24163  tngdsOLD  24164  gausslemma2dlem1a  26865  2lgslem1c  26893  2sqreulem1  26946  2sqreunnlem1  26949  nosupno  27203  nosupbday  27205  nosupbnd1lem5  27212  nosupbnd1  27214  nosupbnd2  27216  noinfno  27218  noinfbday  27220  noinfbnd1lem5  27227  noinfbnd1  27229  noinfbnd2  27231  madess  27368  clwlkclwwlklem2a4  29247  clwlkclwwlklem2a  29248  clwwisshclwwsn  29266  clwwlknon1nloop  29349  eucrctshift  29493  eucrct2eupth  29495  unopbd  31263  nmopcoi  31343  resvsca  32439  resvlem  32440  resvlemOLD  32441  satfv1lem  34348  bj-prmoore  35991  ax12indalem  37810  afvres  45870  afvco2  45874  2ffzoeq  46026  ply1mulgsumlem2  47058  lcoel0  47099  lindslinindsimp1  47128  difmodm1lt  47198  digexp  47283  dig1  47284  itsclc0yqsol  47440