Theorem pm4.71rd 563

Description: Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 10-Feb-2005.)

Hypothesis

Ref	Expression
pm4.71rd.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
pm4.71rd	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜓)))

Proof of Theorem pm4.71rd

Step	Hyp	Ref	Expression
1		pm4.71rd.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	pm4.71d 562	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒)))
3	2	biancomd 464	1 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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:  reueubd  3368  2reu5  3703  ralss  4001  rexss  4002  reuhypd  5359  exopxfr2  5780  dfco2a  6178  feu  6695  fcnvres  6696  funbrfv2b  6877  dffn5  6878  feqmptdf  6889  eqfnfv2  6960  dff4  7027  fmptco  7051  dff13  7178  opiota  7959  mpoxopovel  8098  brtpos  8113  dftpos3  8122  erinxp  8643  qliftfun  8654  pw2f1olem  8933  infm3  12027  prime  12494  predfz  13474  hashf1lem2  14262  hashle2prv  14284  oddnn02np1  16148  oddge22np1  16149  evennn02n  16150  evennn2n  16151  smueqlem  16288  vdwmc2  16769  acsfiel  17452  subsubc  17657  ismgmid  18438  eqger  18894  eqgid  18896  gaorber  19002  symgfix2  19112  znleval  20860  psrbaglefi  21233  psrbaglefiOLD  21234  bastop2  22242  elcls2  22323  maxlp  22396  restopn2  22426  restdis  22427  1stccn  22712  tx1cn  22858  tx2cn  22859  imasnopn  22939  imasncld  22940  imasncls  22941  idqtop  22955  tgqtop  22961  filuni  23134  uffix2  23173  cnflf  23251  isfcls  23258  fclsopn  23263  cnfcf  23291  ptcmplem2  23302  xmeter  23684  imasf1oxms  23743  prdsbl  23745  caucfil  24545  cfilucfil4  24583  shft2rab  24770  sca2rab  24774  mbfinf  24927  i1f1lem  24951  i1fres  24968  itg1climres  24977  mbfi1fseqlem4  24981  iblpos  25055  itgposval  25058  cnplimc  25149  ply1remlem  25425  plyremlem  25562  dvdsflsumcom  26435  fsumvma2  26460  vmasum  26462  logfac2  26463  chpchtsum  26465  logfaclbnd  26468  lgsquadlem1  26626  lgsquadlem2  26627  lgsquadlem3  26628  dchrisum0lem1  26762  colinearalg  27508  nbusgreledg  27950  nbusgredgeu0  27965  umgr2v2enb1  28123  iswwlksnx  28434  wspniunwspnon  28517  clwlknf1oclwwlknlem2  28675  clwlknf1oclwwlkn  28677  eupth2lem2  28812  eupth2lems  28831  frgrncvvdeqlem2  28893  fusgr2wsp2nb  28927  fusgreg2wsp  28929  pjpreeq  29989  elnlfn  30519  eqrrabd  31078  nfpconfp  31195  fimarab  31208  fmptcof2  31222  dfcnv2  31241  2ndpreima  31268  f1od2  31284  fpwrelmap  31296  iocinioc2  31328  nndiffz1  31335  indpi1  32227  1stmbfm  32468  2ndmbfm  32469  eulerpartlemgh  32586  bnj1171  33220  mrsubrn  33715  onunel  33923  elfuns  34308  fneval  34632  bj-imdirval3  35453  topdifinfindis  35615  uncf  35854  phpreu  35859  poimirlem23  35898  poimirlem26  35901  poimirlem27  35902  areacirclem5  35967  erimeq2  36938  prter3  37142  islshpat  37277  lfl1dim  37381  glbconxN  37639  cdlemefrs29bpre0  38657  dib1dim  39426  dib1dim2  39429  diclspsn  39455  dihopelvalcpre  39509  dih1dimatlem  39590  mapdordlem1a  39895  hdmapoc  40192  prjspeclsp  40701  rmydioph  41087  pw2f1ocnv  41110  rfovcnvf1od  41922  ntrneineine0lem  42003  funbrafv2b  44991  dfafn5a  44992  prprelb  45308