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  noel  4284  uni0  4896  axnulALT  5258  axnul  5259  cnv0  5861  cnv0OLD  5862  imadif  6622  poxp3  8160  1div0  11968  xrltnr  13241  nltmnf  13251  0nelfz1  13669  smu01  16649  3lcm2e6woprm  16783  6lcm4e12  16784  join0  18570  meet0  18571  nsmndex1  19105  smndex2dnrinv  19107  degenmgmnfn  19129  degenmgm2nfun  19132  zringndrg  21767  zclmncvs  25462  nolt02o  28045  nogt01o  28046  legso  29055  rgrx0ndm  30167  wwlksnext  30475  ntrl2v2e  30752  avril1  31057  helloworld  31059  topnfbey  31063  xrge00  33568  axnulALT2  35704  axsepg3ALT  35793  fmlaomn0  36134  gonan0  36136  goaln0  36137  prv0  36174  dfon2lem7  36531  nandsym1  37190  bj-inftyexpitaudisj  38106  padd01  40848  ifpdfan  44451  sucomisnotcard  44529  clsk1indlem4  45029  iblempty  46944  salexct2  47318  0nodd  49236  2nodd  49238  1neven  49304  ipolub00  50070