Theorem intnan 486

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 484	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜑)
3	1, 2	mto 197	1 ⊢ ¬ (𝜓 ∧ 𝜑)

Syntax hints:  ¬ wn 3   ∧ 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:  bianfi  533  noel  4304  axnulALT  5262  axnul  5263  cnv0  6116  imadif  6603  poxp3  8132  1div0  11844  xrltnr  13086  nltmnf  13096  0nelfz1  13511  smu01  16463  3lcm2e6woprm  16592  6lcm4e12  16593  join0  18371  meet0  18372  nsmndex1  18847  smndex2dnrinv  18849  zringndrg  21385  zclmncvs  25055  nolt02o  27614  nogt01o  27615  legso  28533  rgrx0ndm  29528  wwlksnext  29830  ntrl2v2e  30094  avril1  30399  helloworld  30401  topnfbey  30405  xrge00  32960  axsepg2ALT  35080  fmlaomn0  35384  gonan0  35386  goaln0  35387  prv0  35424  dfon2lem7  35784  nandsym1  36417  bj-inftyexpitaudisj  37200  padd01  39812  ifpdfan  43462  sucomisnotcard  43540  clsk1indlem4  44040  iblempty  45970  salexct2  46344  0nodd  48162  2nodd  48164  1neven  48230  ipolub00  48985