Theorem intnan 487

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

Syntax hints:  ¬ wn 3   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  bianfi  534  indifdirOLD  4284  noel  4329  noelOLD  4330  axnulALT  5303  axnul  5304  cnv0  6137  imadif  6629  poxp3  8132  xrltnr  13095  nltmnf  13105  0nelfz1  13516  smu01  16423  3lcm2e6woprm  16548  6lcm4e12  16549  join0  18354  meet0  18355  nsmndex1  18790  smndex2dnrinv  18792  zringndrg  21029  zclmncvs  24656  nolt02o  27187  nogt01o  27188  legso  27839  rgrx0ndm  28839  wwlksnext  29136  ntrl2v2e  29400  avril1  29705  helloworld  29707  topnfbey  29711  xrge00  32174  fmlaomn0  34369  gonan0  34371  goaln0  34372  prv0  34409  dfon2lem7  34749  nandsym1  35295  bj-inftyexpitaudisj  36074  padd01  38670  ifpdfan  42202  sucomisnotcard  42280  clsk1indlem4  42780  iblempty  44667  salexct2  45041  0nodd  46566  2nodd  46568  1neven  46783  ipolub00  47571