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  4802  csbexg  5245  snopeqop  5460  xpcan2  6141  tfindsg  7812  findsg  7848  ixpexg  8870  fipwss  9342  ranklim  9768  fin23lem14  10255  fzoval  13614  modsumfzodifsn  13906  hashge2el2dif  14442  iswrdi  14479  swrd0  14621  swrdsbslen  14627  swrdspsleq  14628  pfxccatin12  14695  swrdccat  14697  pfxccat3a  14700  repswswrd  14746  cshword  14753  cshwcsh2id  14790  dvdsabseq  16282  m1exp1  16345  flodddiv4  16384  dfgcd2  16515  lcmftp  16605  prmop1  17009  fvprmselelfz  17015  ressbas  17206  resseqnbas  17212  ressinbas  17215  cntzval  19296  symg2bas  19368  sralem  21171  srasca  21175  sravsca  21176  sraip  21177  ocvval  21647  dsmmval  21714  dmatmul  22462  1mavmul  22513  mavmul0g  22518  1marepvmarrepid  22540  smadiadetglem2  22637  1elcpmat  22680  decpmatid  22735  tnglem  24605  tngds  24613  gausslemma2dlem1a  27328  2lgslem1c  27356  2sqreulem1  27409  2sqreunnlem1  27412  nosupno  27667  nosupbday  27669  nosupbnd1lem5  27676  nosupbnd1  27678  nosupbnd2  27680  noinfno  27682  noinfbday  27684  noinfbnd1lem5  27691  noinfbnd1  27693  noinfbnd2  27695  madess  27858  abssge0  28237  clwlkclwwlklem2a4  30067  clwlkclwwlklem2a  30068  clwwisshclwwsn  30086  clwwlknon1nloop  30169  eucrctshift  30313  eucrct2eupth  30315  unopbd  32086  nmopcoi  32166  resvsca  33392  resvlem  33393  satfv1lem  35544  bj-prmoore  37427  ax12indalem  39391  afvres  47620  afvco2  47624  2ffzoeq  47776  difmodm1lt  47813  ply1mulgsumlem2  48863  lcoel0  48904  lindslinindsimp1  48933  digexp  49083  dig1  49084  itsclc0yqsol  49240