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  3370  2reu5  3719  ralss  4019  rexss  4020  reuhypd  5379  exopxfr2  5805  dfco2a  6203  onunel  6427  feu  6723  fcnvres  6724  funbrfv2b  6905  dffn5  6906  feqmptdf  6917  eqfnfv2  6988  dff4  7056  fmptco  7080  dff13  7207  opiota  7996  mpoxopovel  8156  brtpos  8171  dftpos3  8180  erinxp  8737  qliftfun  8748  pw2f1olem  9027  infm3  12123  prime  12593  predfz  13576  hashf1lem2  14367  hashle2prv  14389  oddnn02np1  16241  oddge22np1  16242  evennn02n  16243  evennn2n  16244  smueqlem  16381  vdwmc2  16862  acsfiel  17548  subsubc  17753  ismgmid  18534  eqger  18994  eqgid  18996  gaorber  19102  symgfix2  19212  znleval  20998  psrbaglefi  21371  psrbaglefiOLD  21372  bastop2  22381  elcls2  22462  maxlp  22535  restopn2  22565  restdis  22566  1stccn  22851  tx1cn  22997  tx2cn  22998  imasnopn  23078  imasncld  23079  imasncls  23080  idqtop  23094  tgqtop  23100  filuni  23273  uffix2  23312  cnflf  23390  isfcls  23397  fclsopn  23402  cnfcf  23430  ptcmplem2  23441  xmeter  23823  imasf1oxms  23882  prdsbl  23884  caucfil  24684  cfilucfil4  24722  shft2rab  24909  sca2rab  24913  mbfinf  25066  i1f1lem  25090  i1fres  25107  itg1climres  25116  mbfi1fseqlem4  25120  iblpos  25194  itgposval  25197  cnplimc  25288  ply1remlem  25564  plyremlem  25701  dvdsflsumcom  26574  fsumvma2  26599  vmasum  26601  logfac2  26602  chpchtsum  26604  logfaclbnd  26607  lgsquadlem1  26765  lgsquadlem2  26766  lgsquadlem3  26767  dchrisum0lem1  26901  colinearalg  27922  nbusgreledg  28364  nbusgredgeu0  28379  umgr2v2enb1  28537  iswwlksnx  28848  wspniunwspnon  28931  clwlknf1oclwwlknlem2  29089  clwlknf1oclwwlkn  29091  eupth2lem2  29226  eupth2lems  29245  frgrncvvdeqlem2  29307  fusgr2wsp2nb  29341  fusgreg2wsp  29343  pjpreeq  30403  elnlfn  30933  eqrrabd  31494  nfpconfp  31613  fimarab  31626  fmptcof2  31640  dfcnv2  31659  2ndpreima  31689  f1od2  31706  fpwrelmap  31718  iocinioc2  31750  nndiffz1  31757  ghmqusker  32272  indpi1  32708  1stmbfm  32949  2ndmbfm  32950  eulerpartlemgh  33067  bnj1171  33701  mrsubrn  34194  elfuns  34576  fneval  34900  bj-imdirval3  35728  topdifinfindis  35890  uncf  36130  phpreu  36135  poimirlem23  36174  poimirlem26  36177  poimirlem27  36178  areacirclem5  36243  erimeq2  37213  prter3  37417  islshpat  37552  lfl1dim  37656  glbconxN  37914  cdlemefrs29bpre0  38932  dib1dim  39701  dib1dim2  39704  diclspsn  39730  dihopelvalcpre  39784  dih1dimatlem  39865  mapdordlem1a  40170  hdmapoc  40467  prjspeclsp  41008  rmydioph  41396  pw2f1ocnv  41419  onsupeqnmax  41639  orddif0suc  41661  cantnf2  41718  tfsconcat0i  41738  rfovcnvf1od  42398  ntrneineine0lem  42477  funbrafv2b  45511  dfafn5a  45512  prprelb  45828