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  4817  csbexg  5257  snopeqop  5462  xpcan2  6143  tfindsg  7813  findsg  7849  ixpexg  8872  fipwss  9344  ranklim  9768  fin23lem14  10255  fzoval  13588  modsumfzodifsn  13879  hashge2el2dif  14415  iswrdi  14452  swrd0  14594  swrdsbslen  14600  swrdspsleq  14601  pfxccatin12  14668  swrdccat  14670  pfxccat3a  14673  repswswrd  14719  cshword  14726  cshwcsh2id  14763  dvdsabseq  16252  m1exp1  16315  flodddiv4  16354  dfgcd2  16485  lcmftp  16575  prmop1  16978  fvprmselelfz  16984  ressbas  17175  resseqnbas  17181  ressinbas  17184  cntzval  19262  symg2bas  19334  sralem  21140  srasca  21144  sravsca  21145  sraip  21146  ocvval  21634  dsmmval  21701  dmatmul  22453  1mavmul  22504  mavmul0g  22509  1marepvmarrepid  22531  smadiadetglem2  22628  1elcpmat  22671  decpmatid  22726  tnglem  24596  tngds  24604  gausslemma2dlem1a  27344  2lgslem1c  27372  2sqreulem1  27425  2sqreunnlem1  27428  nosupno  27683  nosupbday  27685  nosupbnd1lem5  27692  nosupbnd1  27694  nosupbnd2  27696  noinfno  27698  noinfbday  27700  noinfbnd1lem5  27707  noinfbnd1  27709  noinfbnd2  27711  madess  27874  abssge0  28253  clwlkclwwlklem2a4  30084  clwlkclwwlklem2a  30085  clwwisshclwwsn  30103  clwwlknon1nloop  30186  eucrctshift  30330  eucrct2eupth  30332  unopbd  32102  nmopcoi  32182  resvsca  33424  resvlem  33425  satfv1lem  35575  bj-prmoore  37365  ax12indalem  39318  afvres  47529  afvco2  47533  2ffzoeq  47684  difmodm1lt  47716  ply1mulgsumlem2  48744  lcoel0  48785  lindslinindsimp1  48814  digexp  48964  dig1  48965  itsclc0yqsol  49121