Theorem intnan 492

Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.)

Hypothesis

Ref	Expression
intnan.1	⊢ ¬ 𝜑

Assertion

Ref	Expression
intnan	⊢ ¬ (𝜓 ∧ 𝜑)

Proof of Theorem intnan

Step	Hyp	Ref	Expression
1		intnan.1	. 2 ⊢ ¬ 𝜑
2		simpr 490	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜑)
3	1, 2	mto 200	1 ⊢ ¬ (𝜓 ∧ 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  bianfi  543  noelOLD  4287  uni0  4901  axnulALT  5264  axnul  5265  cnv0  5873  cnv0OLD  5874  imadif  6654  poxp3  8204  1div0  12015  xrltnr  13288  nltmnf  13298  0nelfz1  13716  smu01  16700  3lcm2e6woprm  16834  6lcm4e12  16835  join0  18627  meet0  18628  nsmndex1  19162  smndex2dnrinv  19164  degenmgmnfn  19186  degenmgm2nfun  19189  zringndrg  21829  zclmncvs  25524  nolt02o  28109  nogt01o  28110  legso  29119  rgrx0ndm  30231  wwlksnext  30539  ntrl2v2e  30816  avril1  31121  helloworld  31123  topnfbey  31127  xrge00  33674  axnulALT2  35825  axsepg3ALT  35951  fmlaomn0  36363  gonan0  36365  goaln0  36366  prv0  36403  dfon2lem7  36766  nandsym1  37425  bj-inftyexpitaudisj  38394  padd01  41134  ifpdfan  44728  sucomisnotcard  44806  clsk1indlem4  45305  iblempty  47248  salexct2  47622  0nodd  49540  2nodd  49542  1neven  49608  elif0  50253  ipolub00  50438