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  1040  cases2ALT  1048  consensus  1052  preqsnd  4810  csbexg  5249  snopeqop  5449  xpcan2  6126  tfindsg  7794  findsg  7830  ixpexg  8849  fipwss  9319  ranklim  9740  fin23lem14  10227  fzoval  13563  modsumfzodifsn  13851  hashge2el2dif  14387  iswrdi  14424  swrd0  14565  swrdsbslen  14571  swrdspsleq  14572  pfxccatin12  14639  swrdccat  14641  pfxccat3a  14644  repswswrd  14690  cshword  14697  cshwcsh2id  14735  dvdsabseq  16224  m1exp1  16287  flodddiv4  16326  dfgcd2  16457  lcmftp  16547  prmop1  16950  fvprmselelfz  16956  ressbas  17147  resseqnbas  17153  ressinbas  17156  cntzval  19200  symg2bas  19272  sralem  21080  srasca  21084  sravsca  21085  sraip  21086  ocvval  21574  dsmmval  21641  dmatmul  22382  1mavmul  22433  mavmul0g  22438  1marepvmarrepid  22460  smadiadetglem2  22557  1elcpmat  22600  decpmatid  22655  tnglem  24526  tngds  24534  gausslemma2dlem1a  27274  2lgslem1c  27302  2sqreulem1  27355  2sqreunnlem1  27358  nosupno  27613  nosupbday  27615  nosupbnd1lem5  27622  nosupbnd1  27624  nosupbnd2  27626  noinfno  27628  noinfbday  27630  noinfbnd1lem5  27637  noinfbnd1  27639  noinfbnd2  27641  madess  27790  abssge0  28152  clwlkclwwlklem2a4  29941  clwlkclwwlklem2a  29942  clwwisshclwwsn  29960  clwwlknon1nloop  30043  eucrctshift  30187  eucrct2eupth  30189  unopbd  31959  nmopcoi  32039  resvsca  33271  resvlem  33272  satfv1lem  35345  bj-prmoore  37099  ax12indalem  38934  afvres  47166  afvco2  47170  2ffzoeq  47321  difmodm1lt  47353  ply1mulgsumlem2  48382  lcoel0  48423  lindslinindsimp1  48452  digexp  48602  dig1  48603  itsclc0yqsol  48759