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

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

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 210  df-an 400

This theorem is referenced by:  4cases  1036  cases2ALT  1044  consensus  1048  preqsnd  4749  csbexg  5178  snopeqop  5361  xpcan2  6001  tfindsg  7555  findsg  7590  ixpexg  8469  fipwss  8877  ranklim  9257  fin23lem14  9744  fzoval  13034  modsumfzodifsn  13307  hashge2el2dif  13834  iswrdi  13861  swrd0  14011  swrdsbslen  14017  swrdspsleq  14018  pfxccatin12  14086  swrdccat  14088  pfxccat3a  14091  repswswrd  14137  cshword  14144  cshwcsh2id  14181  dvdsabseq  15655  m1exp1  15717  flodddiv4  15754  dfgcd2  15884  lcmftp  15970  prmop1  16364  fvprmselelfz  16370  ressbas  16546  resslem  16549  ressinbas  16552  cntzval  18443  symg2bas  18513  sralem  19942  srasca  19946  sravsca  19947  sraip  19948  ocvval  20356  dsmmval  20423  dmatmul  21102  1mavmul  21153  mavmul0g  21158  1marepvmarrepid  21180  smadiadetglem2  21277  1elcpmat  21320  decpmatid  21375  tnglem  23246  tngds  23254  gausslemma2dlem1a  25949  2lgslem1c  25977  2sqreulem1  26030  2sqreunnlem1  26033  clwlkclwwlklem2a4  27782  clwlkclwwlklem2a  27783  clwwisshclwwsn  27801  clwwlknon1nloop  27884  eucrctshift  28028  eucrct2eupth  28030  unopbd  29798  nmopcoi  29878  resvsca  30954  resvlem  30955  satfv1lem  32722  noprefixmo  33315  nosupno  33316  nosupbday  33318  nosupbnd1lem5  33325  nosupbnd1  33327  nosupbnd2  33329  bj-prmoore  34530  ax12indalem  36241  afvres  43728  afvco2  43732  2ffzoeq  43885  ply1mulgsumlem2  44795  lcoel0  44837  lindslinindsimp1  44866  difmodm1lt  44936  digexp  45021  dig1  45022  itsclc0yqsol  45178