Theorem pm4.71rd 572

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  reueubd  3383  2reu5  3716  ralss  4004  rexss  4005  ralssOLD  4006  rexssOLD  4007  eqrrabd  4034  rabsneq  4603  reuhypd  5381  exopxfr2  5822  dfrn7  6066  dfco2a  6247  onunel  6470  feu  6758  fcnvres  6759  funbrfv2b  6942  dffn5  6943  feqmptdf  6955  fimarab  6959  eqfnfv2  7030  dff4  7101  fmptco  7130  dff13  7258  opiota  8070  mpoxopovel  8237  brtpos  8252  dftpos3  8261  erinxp  8812  qliftfun  8823  uncf  8891  pw2f1olem  9100  elirrv  9591  infm3  12276  indpi1  12334  prime  12780  predfz  13787  hashf1lem2  14601  hashle2prv  14623  oddnn02np1  16518  oddge22np1  16519  evennn02n  16520  evennn2n  16521  smueqlem  16660  vdwmc2  17157  acsfiel  17828  subsubc  18028  ismgmid  18845  eqger  19390  eqgid  19392  ghmqusker  19501  gaorber  19522  symgfix2  19630  rspsn0  21526  isfieldidl  21540  znleval  21860  psrbaglefi  22234  bastop2  23312  elcls2  23392  maxlp  23465  restopn2  23495  restdis  23496  1stccn  23782  tx1cn  23928  tx2cn  23929  imasnopn  24009  imasncld  24010  imasncls  24011  idqtop  24025  tgqtop  24031  filuni  24204  uffix2  24243  cnflf  24321  isfcls  24328  fclsopn  24333  cnfcf  24361  ptcmplem2  24372  xmeter  24752  imasf1oxms  24808  prdsbl  24810  caucfil  25604  cfilucfil4  25642  shft2rab  25829  sca2rab  25833  mbfinf  25986  i1f1lem  26010  i1fres  26026  itg1climres  26035  mbfi1fseqlem4  26039  iblpos  26113  itgposval  26116  cnplimc  26207  ply1remlem  26483  plyremlem  26625  dvdsflsumcom  27515  fsumvma2  27541  vmasum  27543  logfac2  27544  chpchtsum  27546  logfaclbnd  27549  lgsquadlem1  27707  lgsquadlem2  27708  lgsquadlem3  27709  dchrisum0lem1  27843  colinearalg  29488  nbusgreledg  29934  nbusgredgeu0  29949  umgr2v2enb1  30107  iswwlksnx  30429  wspniunwspnon  30512  clwlknf1oclwwlknlem2  30673  clwlknf1oclwwlkn  30675  eupth2lem2  30820  eupth2lems  30839  frgrncvvdeqlem2  30901  fusgr2wsp2nb  30935  fusgreg2wsp  30937  pjpreeq  32000  elnlfn  32530  nfpconfp  33226  fmptcof2  33251  dfcnv2  33269  2ndpreima  33301  f1od2  33311  fpwrelmap  33325  iocinioc2  33371  nndiffz1  33378  algextdeglem6  34354  1stmbfm  34892  2ndmbfm  34893  eulerpartlemgh  35010  bnj1171  35630  mrsubrn  36278  elfuns  36677  fneval  37140  mh-regprimbi  37333  bj-imdirval3  38105  topdifinfindis  38269  phpreu  38527  poimirlem23  38561  poimirlem26  38564  poimirlem27  38565  areacirclem5  38630  erimeq2  39695  prter3  39939  islshpat  40074  lfl1dim  40178  glbconxN  40435  cdlemefrs29bpre0  41453  dib1dim  42222  dib1dim2  42225  diclspsn  42251  dihopelvalcpre  42305  dih1dimatlem  42386  mapdordlem1a  42691  hdmapoc  42988  prjspeclsp  43640  rmydioph  44020  pw2f1ocnv  44043  onsupeqnmax  44248  orddif0suc  44269  cantnf2  44326  tfsconcat0i  44346  rfovcnvf1od  45003  ntrneineine0lem  45082  modelaxreplem3  45969  funbrafv2b  48228  dfafn5a  48229  prprelb  48597  stgredgiun  49055  gpgiedgdmel  49146  gpgedgel  49147