Theorem intnan 488

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

Syntax hints:  ¬ wn 3   ∧ wa 397

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 398

This theorem is referenced by:  bianfi  535  indifdirOLD  4286  noel  4331  noelOLD  4332  axnulALT  5305  axnul  5306  cnv0  6141  imadif  6633  poxp3  8136  xrltnr  13099  nltmnf  13109  0nelfz1  13520  smu01  16427  3lcm2e6woprm  16552  6lcm4e12  16553  join0  18358  meet0  18359  nsmndex1  18794  smndex2dnrinv  18796  zringndrg  21038  zclmncvs  24665  nolt02o  27198  nogt01o  27199  legso  27850  rgrx0ndm  28850  wwlksnext  29147  ntrl2v2e  29411  avril1  29716  helloworld  29718  topnfbey  29722  xrge00  32187  fmlaomn0  34381  gonan0  34383  goaln0  34384  prv0  34421  dfon2lem7  34761  nandsym1  35307  bj-inftyexpitaudisj  36086  padd01  38682  ifpdfan  42217  sucomisnotcard  42295  clsk1indlem4  42795  iblempty  44681  salexct2  45055  0nodd  46580  2nodd  46582  1neven  46830  ipolub00  47618