Theorem pm4.71rd 564

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 563	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒)))
3	2	biancomd 465	1 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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:  reueubd  3396  2reu5  3755  ralss  4055  rexss  4056  reuhypd  5418  exopxfr2  5845  dfco2a  6246  onunel  6470  feu  6768  fcnvres  6769  funbrfv2b  6950  dffn5  6951  feqmptdf  6963  eqfnfv2  7034  dff4  7103  fmptco  7127  dff13  7254  opiota  8045  mpoxopovel  8205  brtpos  8220  dftpos3  8229  erinxp  8785  qliftfun  8796  pw2f1olem  9076  infm3  12173  prime  12643  predfz  13626  hashf1lem2  14417  hashle2prv  14439  oddnn02np1  16291  oddge22np1  16292  evennn02n  16293  evennn2n  16294  smueqlem  16431  vdwmc2  16912  acsfiel  17598  subsubc  17803  ismgmid  18584  eqger  19058  eqgid  19060  gaorber  19172  symgfix2  19284  znleval  21110  psrbaglefi  21485  psrbaglefiOLD  21486  bastop2  22497  elcls2  22578  maxlp  22651  restopn2  22681  restdis  22682  1stccn  22967  tx1cn  23113  tx2cn  23114  imasnopn  23194  imasncld  23195  imasncls  23196  idqtop  23210  tgqtop  23216  filuni  23389  uffix2  23428  cnflf  23506  isfcls  23513  fclsopn  23518  cnfcf  23546  ptcmplem2  23557  xmeter  23939  imasf1oxms  23998  prdsbl  24000  caucfil  24800  cfilucfil4  24838  shft2rab  25025  sca2rab  25029  mbfinf  25182  i1f1lem  25206  i1fres  25223  itg1climres  25232  mbfi1fseqlem4  25236  iblpos  25310  itgposval  25313  cnplimc  25404  ply1remlem  25680  plyremlem  25817  dvdsflsumcom  26692  fsumvma2  26717  vmasum  26719  logfac2  26720  chpchtsum  26722  logfaclbnd  26725  lgsquadlem1  26883  lgsquadlem2  26884  lgsquadlem3  26885  dchrisum0lem1  27019  colinearalg  28168  nbusgreledg  28610  nbusgredgeu0  28625  umgr2v2enb1  28783  iswwlksnx  29094  wspniunwspnon  29177  clwlknf1oclwwlknlem2  29335  clwlknf1oclwwlkn  29337  eupth2lem2  29472  eupth2lems  29491  frgrncvvdeqlem2  29553  fusgr2wsp2nb  29587  fusgreg2wsp  29589  pjpreeq  30651  elnlfn  31181  eqrrabd  31741  nfpconfp  31856  fimarab  31868  fmptcof2  31882  dfcnv2  31901  2ndpreima  31929  f1od2  31946  fpwrelmap  31958  iocinioc2  31990  nndiffz1  31997  ghmqusker  32532  indpi1  33018  1stmbfm  33259  2ndmbfm  33260  eulerpartlemgh  33377  bnj1171  34011  mrsubrn  34504  elfuns  34887  fneval  35237  bj-imdirval3  36065  topdifinfindis  36227  uncf  36467  phpreu  36472  poimirlem23  36511  poimirlem26  36514  poimirlem27  36515  areacirclem5  36580  erimeq2  37548  prter3  37752  islshpat  37887  lfl1dim  37991  glbconxN  38249  cdlemefrs29bpre0  39267  dib1dim  40036  dib1dim2  40039  diclspsn  40065  dihopelvalcpre  40119  dih1dimatlem  40200  mapdordlem1a  40505  hdmapoc  40802  prjspeclsp  41354  rmydioph  41753  pw2f1ocnv  41776  onsupeqnmax  41996  orddif0suc  42018  cantnf2  42075  tfsconcat0i  42095  rfovcnvf1od  42755  ntrneineine0lem  42834  funbrafv2b  45867  dfafn5a  45868  prprelb  46184