Theorem con2bid 354

Description: A contraposition deduction. (Contributed by NM, 15-Apr-1995.)

Hypothesis

Ref	Expression
con2bid.1	⊢ (𝜑 → (𝜓 ↔ ¬ 𝜒))

Assertion

Ref	Expression
con2bid	⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓))

Proof of Theorem con2bid

Step	Hyp	Ref	Expression
1		con2bid.1	. 2 ⊢ (𝜑 → (𝜓 ↔ ¬ 𝜒))
2		con2bi 353	. 2 ⊢ ((𝜒 ↔ ¬ 𝜓) ↔ (𝜓 ↔ ¬ 𝜒))
3	1, 2	sylibr 233	1 ⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205

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

This theorem is referenced by:  con1bid  355  sotric  5612  sotrieq  5613  sotr2  5616  isso2i  5619  sotr3  5623  sotri2  6129  sotri3  6130  somin1  6133  somincom  6134  ordtri2  6398  ordtr3  6408  ordintdif  6413  ord0eln0  6418  soisoi  7330  weniso  7356  ordunisuc2  7842  limsssuc  7848  nlimon  7849  tfrlem15  8406  oawordeulem  8568  nnawordex  8651  onomeneqOLD  9247  fimaxg  9308  suplub2  9478  fiming  9515  wemapsolem  9567  cantnflem1  9706  rankval3b  9843  cardsdomel  9991  harsdom  10012  isfin1-2  10402  fin1a2lem7  10423  suplem2pr  11070  xrltnle  11305  ltnle  11317  leloe  11324  xrlttri  13144  xrleloe  13149  xrrebnd  13173  supxrbnd2  13327  supxrbnd  13333  om2uzf1oi  13944  rabssnn0fi  13977  cnpart  15213  bits0e  16397  bitsmod  16404  bitsinv1lem  16409  sadcaddlem  16425  trfil2  23784  xrsxmet  24718  metdsge  24758  ovolunlem1a  25418  ovolunlem1  25419  itg2seq  25665  noetasuplem4  27662  noetainflem4  27666  sltnle  27679  sleloe  27680  toslublem  32693  tosglblem  32695  isarchi2  32887  gsumesum  33672  sgnneg  34154  elfuns  35505  finminlem  35796  bj-bibibi  36057  itg2addnclem  37138  heiborlem10  37287  aks4d1p8  41552  cantnfresb  42747  naddwordnexlem4  42825  ontric3g  42946  or3or  43447  ntrclselnel2  43482  clsneifv3  43534  islininds2  47546

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »