Theorem pm4.71rd 562

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  reueubd  3370  2reu5  3726  ralss  4018  rexss  4019  ralssOLD  4020  rexssOLD  4021  eqrrabd  4045  rabsneq  4604  reuhypd  5369  exopxfr2  5798  dfco2a  6207  onunel  6427  feu  6718  fcnvres  6719  funbrfv2b  6900  dffn5  6901  feqmptdf  6913  fimarab  6917  eqfnfv2  6986  dff4  7055  fmptco  7083  dff13  7211  opiota  8017  mpoxopovel  8176  brtpos  8191  dftpos3  8200  erinxp  8741  qliftfun  8752  pw2f1olem  9022  infm3  12118  prime  12591  predfz  13590  hashf1lem2  14397  hashle2prv  14419  oddnn02np1  16294  oddge22np1  16295  evennn02n  16296  evennn2n  16297  smueqlem  16436  vdwmc2  16926  acsfiel  17595  subsubc  17795  ismgmid  18574  eqger  19092  eqgid  19094  ghmqusker  19201  gaorber  19222  symgfix2  19330  znleval  21496  psrbaglefi  21868  bastop2  22914  elcls2  22994  maxlp  23067  restopn2  23097  restdis  23098  1stccn  23383  tx1cn  23529  tx2cn  23530  imasnopn  23610  imasncld  23611  imasncls  23612  idqtop  23626  tgqtop  23632  filuni  23805  uffix2  23844  cnflf  23922  isfcls  23929  fclsopn  23934  cnfcf  23962  ptcmplem2  23973  xmeter  24354  imasf1oxms  24410  prdsbl  24412  caucfil  25216  cfilucfil4  25254  shft2rab  25442  sca2rab  25446  mbfinf  25599  i1f1lem  25623  i1fres  25639  itg1climres  25648  mbfi1fseqlem4  25652  iblpos  25727  itgposval  25730  cnplimc  25821  ply1remlem  26103  plyremlem  26245  dvdsflsumcom  27131  fsumvma2  27158  vmasum  27160  logfac2  27161  chpchtsum  27163  logfaclbnd  27166  lgsquadlem1  27324  lgsquadlem2  27325  lgsquadlem3  27326  dchrisum0lem1  27460  colinearalg  28890  nbusgreledg  29333  nbusgredgeu0  29348  umgr2v2enb1  29507  iswwlksnx  29820  wspniunwspnon  29903  clwlknf1oclwwlknlem2  30061  clwlknf1oclwwlkn  30063  eupth2lem2  30198  eupth2lems  30217  frgrncvvdeqlem2  30279  fusgr2wsp2nb  30313  fusgreg2wsp  30315  pjpreeq  31377  elnlfn  31907  nfpconfp  32606  fmptcof2  32631  dfcnv2  32650  2ndpreima  32681  f1od2  32694  fpwrelmap  32706  iocinioc2  32752  nndiffz1  32759  indpi1  32833  algextdeglem6  33705  1stmbfm  34244  2ndmbfm  34245  eulerpartlemgh  34362  bnj1171  34983  mrsubrn  35493  elfuns  35896  fneval  36333  bj-imdirval3  37165  topdifinfindis  37327  uncf  37586  phpreu  37591  poimirlem23  37630  poimirlem26  37633  poimirlem27  37634  areacirclem5  37699  erimeq2  38663  prter3  38868  islshpat  39003  lfl1dim  39107  glbconxN  39365  cdlemefrs29bpre0  40383  dib1dim  41152  dib1dim2  41155  diclspsn  41181  dihopelvalcpre  41235  dih1dimatlem  41316  mapdordlem1a  41621  hdmapoc  41918  prjspeclsp  42593  rmydioph  42996  pw2f1ocnv  43019  onsupeqnmax  43229  orddif0suc  43250  cantnf2  43307  tfsconcat0i  43327  rfovcnvf1od  43986  ntrneineine0lem  44065  modelaxreplem3  44963  funbrafv2b  47153  dfafn5a  47154  prprelb  47510  stgredgiun  47950  gpgiedgdmel  48033  gpgedgel  48034