Theorem intnan 485

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

Syntax hints:  ¬ wn 3   ∧ wa 394

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 395

This theorem is referenced by:  bianfi  532  indifdirOLD  4284  noel  4329  noelOLD  4330  axnulALT  5303  axnul  5304  cnv0  6139  imadif  6631  poxp3  8138  xrltnr  13103  nltmnf  13113  0nelfz1  13524  smu01  16431  3lcm2e6woprm  16556  6lcm4e12  16557  join0  18362  meet0  18363  nsmndex1  18830  smndex2dnrinv  18832  zringndrg  21239  zclmncvs  24896  nolt02o  27434  nogt01o  27435  legso  28117  rgrx0ndm  29117  wwlksnext  29414  ntrl2v2e  29678  avril1  29983  helloworld  29985  topnfbey  29989  xrge00  32454  fmlaomn0  34679  gonan0  34681  goaln0  34682  prv0  34719  dfon2lem7  35065  nandsym1  35610  bj-inftyexpitaudisj  36389  padd01  38985  ifpdfan  42519  sucomisnotcard  42597  clsk1indlem4  43097  iblempty  44979  salexct2  45353  0nodd  46846  2nodd  46848  1neven  46918  ipolub00  47705