Theorem anbi12d 763

Description: Deduction joining two equivalences to form equivalence of conjunctions.

Hypotheses

Ref	Expression
bi12d.1	|- (ph -> (ps <-> ch))
bi12d.2	|- (ph -> (th <-> ta))

Assertion

Ref	Expression
anbi12d	|- (ph -> ((ps /\ th) <-> (ch /\ ta)))

Proof of Theorem anbi12d

Step	Hyp	Ref	Expression
1		bi12d.1	. . 3 |- (ph -> (ps <-> ch))
2	1	anbi1d 752	. 2 |- (ph -> ((ps /\ th) <-> (ch /\ th)))
3		bi12d.2	. . 3 |- (ph -> (th <-> ta))
4	3	anbi2d 751	. 2 |- (ph -> ((ch /\ th) <-> (ch /\ ta)))
5	2, 4	bitrd 284	1 |- (ph -> ((ps /\ th) <-> (ch /\ ta)))

Syntax hints:   -> wi 3   <-> wb 219   /\ wa 337

This theorem is referenced by:  pm4.38 949  3anbi123d 1441  drsb1 1819  mopick 2094  clelab 2262  cbvrexf 2523  cbvreuv 2528  gencbvex 2579  rcla4e 2615  eqvincf 2629  ceqsrexv 2634  elrabf 2653  ralrab 2658  cbvrab 2662  reu2 2688  reu6 2689  rmo4 2691  reu8 2694  reuind 2696  sbcang 2734  sbcabel 2766  cbvrexcsf 2821  cbvreucsf 2822  cbvrabcsf 2823  difjust 2829  injust 2833  eldif 2840  psseq1 2921  psseq2 2922  ssconb 2957  elin 2999  2ralunsn 3358  elunii 3371  csbunig 3374  eluniab 3378  cbvopab 3571  cbvopab1 3573  cbvopab1s 3574  cbvopab2v 3576  trel 3586  nalset 3615  elssabg 3629  intabs 3637  nnullss 3678  exss 3679  opelopab2 3730  dfid3 3748  poeq1 3754  pocl 3756  posn 3762  soeq1 3767  fri 3783  frc 3785  weeq1 3800  weeq2 3801  ordeq 3818  zfun 3930  snnex 3940  reusv2lem4 3970  reusv3 3974  onminex 4031  dflim3 4068  elom 4088  elomg 4089  csbxpg 4160  vtoclr 4167  opbrop 4197  relop 4242  elsnres 4369  asymref2 4424  elxp4 4482  elxp5 4483  funopg 4556  fununi 4582  funcnvuni 4583  fneq1 4602  2elresin 4623  feq1 4647  f1eq1 4692  foeq1 4701  f1oeq1 4718  f1oeq2 4719  f1oeq3 4720  ffoss 4751  fv3 4779  tz6.12f 4784  dffn5 4803  ssimaex 4814  dffv2 4820  fvopab3 4826  fvopab3ig 4827  fvopab4gf 4830  fvopab6 4843  inpreima 4871  opabex3 4933  elunirnALT 4941  isoeq1 4958  isoeq4 4961  isomin 4972  isoini 4973  isofrlem 4974  isowe 4976  f1oiso2 4978  f1oweALT 4980  cbvoprab1 5019  cbvoprab12 5020  oprabval 5045  oprabvalig 5046  oprabval2gf 5049  oprabval4g 5054  oprabval4gALT 5055  caoprmo 5096  mpteq12dv 5101  mpt2eq123dv 5102  cbvmpt 5107  unielxp 5158  dfoprab4s 5167  dfoprab5sf 5169  oprabopabf 5170  frxp 5210  xporderlem 5211  poxp 5212  fnwelem 5215  smoiso 5273  tfrlem1 5282  tfrlem3 5284  tfrlem3a 5285  tfrlem5 5287  tfrlem12 5294  tz7.44-2 5301  tz7.44-3 5302  rdglem2 5310  omeu 5426  oeoa 5438  oeoe 5440  ertr 5492  brecop 5526  ecopoprtrn 5531  th3qlem1 5534  th3qlem2 5535  th3q 5537  elpm 5556  elixp2 5569  ixpeq1 5573  mapsnen 5650  mapsnenOLD 5651  xpsnen 5658  endisj 5660  pw2en 5671  ac6sfi 5675  sbthlem2 5677  sbth 5686  cbvriota 5741  riotasv2d 5760  php2 5800  nnsdomo 5808  isinf 5828  xpfir 5838  fimaxg 5847  unfilem1 5860  unifi 5870  fiint 5872  abfii4 5876  supeq1 5892  supmo 5895  supub 5899  suplub 5900  supmaxlem 5909  suppr 5911  supsnALT 5913  ordiso 5914  ordtypelem1 5915  ordtypelem6 5920  ordtype 5922  hartogslem 5923  en2lp 5939  inf0 5944  axinf2 5963  dfom3 5972  unbnn3 5982  rankr1g 6022  r1pwcl 6034  karden 6095  cardprclem 6134  infxpen 6148  aleph11 6166  aceq1 6183  aceq0 6184  aceq2 6185  aceq3lem 6186  aceq3 6187  aceq4 6188  aceq5lem1 6189  aceq5lem2 6190  aceq5lem3 6191  aceq5lem4 6192  aceq5 6194  aceq6a 6195  aceq6b 6196  fodomnumlem 6208  cdainf 6258  cflem 6265  cfval 6266  cflecard 6272  cfeq0 6275  cfsuc 6276  cfflb 6279  cfsmolem 6285  cfcoflem 6287  coftr 6288  axcc2lem 6293  domtriomlem 6296  domtriomlemOLD 6298  dominf 6300  axdc2lem 6303  axdc2 6304  axdc3lem2 6306  axdc3lem4 6308  zfac 6315  ac7g 6319  ac5 6322  ac6lem 6324  ac6sg 6330  ac6sgOLD 6331  kmlem1 6337  kmlem2 6338  kmlem4 6340  kmlem14 6350  zorn2lem1 6361  zorn2lem7 6367  zorn2 6369  brdom3 6377  brdom7disj 6380  brdom6disj 6381  unidom 6384  cardsdom 6402  alephnbtwn2OLD 6433  dominfac 6445  cfeq0OLD 6446  cfsucOLD 6447  axrepndlem2 6463  axunnd 6466  axregndlem2 6473  axinfndlem1 6475  axacndlem5 6481  axacnd 6482  zfcndun 6485  zfcndac 6489  ltsopi 6534  indpi 6552  ltsopq 6593  ltbtwnpq 6602  elnp 6610  prcdpq 6615  genpv 6620  genpprecl 6622  genpnmax 6628  ltprord 6652  ltsopr 6654  ltexprlem4 6663  ltexprlem7 6666  prlem936 6673  reclem1pr 6674  reclem3pr 6676  supexpr 6681  ltsosr 6721  negexsr 6729  recexsr 6734  suppsr 6740  suppsr3 6742  supsrlem5 6747  supsrlem6 6748  ltresr 6776  supre 6778  ltsor 6779  axrnegex 6799  axrrecex 6800  axcnre 6802  ltxr 6854  axlttrn 6863  axsup 6866  letri3 6876  ltleadd 7167  lesub0 7200  div11 7272  recrec 7283  prodgt0 7335  prodge0 7337  posexi 7424  peano5nni 7442  dfnn2 7452  nn2ge 7458  nominpos 7570  lbinfm 7597  sup2 7600  infm3 7603  dfinfmr 7616  infmsup 7617  nnunb 7619  xrsupsslem 7625  xrinfmsslem 7626  xrsupss 7627  xrinfmss 7628  supxr 7630  zltp1le 7732  z2ge 7743  dfuzi 7757  peano5uzi 7758  uzind 7760  uzindOLD 7763  zmax 7778  rebtwnz 7780  qbtwnre 7805  qbtwnxr 7806  flval 7810  fllelt 7813  flval2 7824  flbi 7826  flbi2 7827  modid2 7859  iooin 7885  elioo1 7891  elioo2 7892  elioc1 7894  elico1 7895  elicc1 7896  iooshf 7910  iooneg 7921  iccneg 7922  icoshft 7923  icoshftf1olem 7925  icounlem 7927  icoun 7928  nnwof 7975  elfz1 8001  fzsuc 8041  fzrev 8052  sqr0 8306  sqrlem4 8310  sqrlem24 8330  sqrgt0ii 8331  sqrlem26 8332  sqr2irrlem2 8359  abslt 8516  absle 8517  absdiflt 8519  absdifle 8520  abs1mi 8541  abs3lem 8544  cau3iri 8552  cau5ii 8554  bcval 8595  clim 8633  dffsum 8654  climuni 8755  climshfti 8760  climresi 8761  iserzshft2i 8763  climrecl 8766  climge0 8768  caucvg3 8824  cvgcmp3cetlem1 8845  cvgcmp3cetlem2 8846  iserzgt0 8868  supcvglem 8876  supcvg 8877  expcnvlem5 8890  explecnv 8893  geolim 8897  geolim1 8899  fsum0diag 8918  cncfval 8924  elcncf 8925  efseq1ex 8966  absef01tlubi 9048  efcnlem4 9085  reeff1olem2 9088  acdc3 9153  acdc2 9157  acdc5 9160  acdc 9162  ruclem4 9176  ruclem12 9184  ruclem29 9201  ruclem36 9208  infxpidmlem2OLD 9216  infxpidmlem3OLD 9217  infxpidmlem8OLD 9222  infpss 9237  infmap2lem1 9242  divalgmod 9303  ndvdssub 9304  gcdcllem2 9313  gcdcllem3 9314  gcddvds 9316  eucalgval 9344  mulgcdlem1 9351  mulgcdlem2 9352  1nprm 9366  isprm3 9370  infpnlem2 9389  infpn2 9391  1arithlem6 9399  1arithlem7 9400  1arithlem30 9424  1arithlem31 9425  isgrp 9464  grplem1 9469  grpideu 9478  isgrpi 9480  grpidval 9482  grpidinv2 9484  grpinvfval 9490  grpinv 9493  ringidval 9507  isring 9508  ringi 9509  ringideu 9512  ringidmlem 9518  ispos 9548  poslem 9549  lubfval 9572  lubval 9573  lubprop 9574  glbfval 9577  glbval 9578  glbprop 9579  joinval2 9583  joinlem 9584  joinle 9587  meetval2 9590  meetlem 9591  meetle 9594  islat 9609  latlem 9610  isclat 9671  clatlem 9672  clatl 9676  lubun 9682  istopg 9700  eltopspOLD 9710  tpsexOLD 9711  istpsOLD 9712  istps 9717  eltpsg 9725  fiinbas 9736  eltg2 9740  tgval3 9746  topbas 9748  subbas 9765  subtop 9767  fctop 9771  cctop 9773  retopbas 9782  cldval 9803  ntrfval 9804  clsfval 9805  iscld 9806  elcls 9844  neifval 9855  isnei 9859  neiint 9860  neips 9868  opnneissb 9869  opnssneib 9870  innei 9878  lpfval 9884  islp2 9889  qdensere 9893  cnpfval 9899  cnpnei 9909  ismet 9941  dfms2 9942  ismsg 9943  msflem 9946  metreslem 9965  blfval 9978  blelrn 9991  blin 9995  blss 9996  blssex 9997  opnfval 10000  opnm 10003  blssopn 10010  opnin 10012  neibl 10020  blnei 10022  metcnp 10031  metcn 10033  metcnpi3 10036  metcnpi4 10037  metcni2 10039  tgioolem 10058  caufval 10070  lmbr 10072  iscau3 10082  iscau4 10084  lmss 10097  lmfex 10103  lmle 10104  metelcls 10109  metcnp4 10114  xpcn 10120  fsumcnlem 10133  iscms2lem4 10136  lmcau 10140  bcthlem2 10144  bcthlem7 10149  bcthlem15 10157  bcth 10176  isgrpo 10187  isgrpo2 10188  grp2grpo 10190  isgrpoi 10191  grpoideu 10202  grpidvallem 10210  grpoidval 10211  grpoidinv2 10213  grpoinvfval 10219  grpoinv 10222  grpdivfval 10235  gxoprval 10249  isgalem 10318  isga 10319  ssga 10324  gapmlem 10330  gapm 10331  isringo 10334  ringoi 10335  ringid 10338  ringoideu 10339  cnring 10358  ringsn 10359  drngi 10362  vci 10368  isvclem 10397  vacnlem3 10538  vacnlem6 10541  vacn 10542  nmcnilem 10545  va1cnlem 10553  sm1cnilem 10555  ipfval 10560  lnoval 10621  islno 10622  nmofval 10633  nmosetn0 10636  nmolb 10642  nmounbseqi 10648  nmlno0lem 10662  blocni 10674  ajmoi 10729  pslem 10861  spwval2 10867  spwmo 10870  spwpr2 10872  spwpr4 10877  spwpr4OLD 10878  spwpr4aOLD 10879  isla 10881  pilem2 10892  pilem3 10893  pilem4 10894  sinperlem2 10907  sincosq1sgn 10924  sincosq2sgn 10925  sincosq3sgn 10926  sincosq4sgn 10927  efifolem2 10948  efifolem3 10949  efifolem6 10952  effoi 10970  elghomlem1 11025  elghomlem2 11026  abfi 11050  uptx 11061  txcnopab 11063  subcld 11092  subtopmetlem 11093  subtopmet 11094  isfil 11104  elfg 11122  fgfil 11128  hausfillim 11141  filmapf 11145  isfilmap 11146  elfilmap 11150  flimff 11155  sflimf 11156  isdir 11190  dirtr 11194  dirge 11195  tosdir 11196  isexid 11202  isexid2 11210  exidu1 11211  idrval 11212  cmpidelt 11214  issmgrp 11219  unmnd 11243  isdivrngo 11255  normlem7tALT 11455  norm3lemt 11488  hcau 11520  hcau2 11524  hlimi 11525  hlim2 11529  sh 11547  closedsub 11560  chlimi 11571  hlimunii 11576  ch2 11581  hhsssh 11606  ocsh 11623  ocin 11636  projlem7 11659  projlem17 11669  projlem26 11678  projlem28 11680  pjtheu 11703  pjmval 11705  omlsi 11713  pjoml 11736  shintcl 11761  chintcl 11763  shlub 11821  chpsscon3 11893  cmbr 11992  pjoml6i 11997  cm2j 12028  spansncv 12065  pjrni 12114  adjmo 12227  eigre 12230  eigorth 12233  elcnop 12252  ellnop 12253  nmopsetn0 12261  elunop 12268  elhmop 12269  nmfnsetn0 12274  elcnfn 12278  ellnfn 12279  eigvalval 12292  nmoplb 12300  nmfnlb 12317  eleigvec 12350  0cnop 12372  0cnfn 12373  idcnop 12374  nmlnop0iALT 12389  lnophm 12413  lnopconi 12432  nmbdfnlb 12448  lnfnconi 12459  branmfn 12507  bra11 12510  leopg 12524  leoptri 12538  leoptr 12539  opsqrlem1 12542  hmopidmch 12556  hmopidmpj 12557  elpjrnch 12594  stel 12617  hstel 12618  hstel2 12622  jpi 12673  cvbr 12685  cvcon3 12687  cvnbtwn 12689  mdbr 12697  dmdbr 12702  mdsl1i 12724  mdslmd1lem3 12730  mdslmd1lem4 12731  csmdsymi 12737  elat2 12743  chrelati 12767  chrelat2i 12768  cvexchlem 12771  irred 12798  atcvat4i 12800  mdsymlem2 12807  mdsymlem8 12813  mddmdin0i 12834  cdj1i 12836  cdj3i 12844  bnj148 13261  bnj919 13600  bnj1185 13738  bnj1273 13800  bnj1306 13820  bnj1310 13821  bnj1401 13884  bnj1484 13930  bnj1492 13932  bnj64 13972  bnj1014 14145  bnj1015 14146  bnj1112 14189  bnj1152 14208  bnj1154 14209  bnj1228 14227  bnj1234 14231  bnj1321 14269  bnj1462 14317  bnj1463 14321  bnj1491 14327  sindivcvglem2 14387  sindivcvglem8 14393  sindivcvg 14394  circumlem3 14397  fseq1cl 14409  elsnresOLD 14455  dfpo2 14465  fununiq 14476  dfon2lem3 14485  dfon2lem4 14486  dfon2lem5 14487  dfon2lem6 14488  dfon2lem7 14489  dfon2lem8 14490  dfon2 14492  tz6.26 14558  frmin 14591  xporderlemOLD 14601  poxpOLD 14602  frxpOLD 14604  poseq 14607  soseq 14608  wfr3g 14609  wfrlem1 14610  wfrlem4 14613  wfrlem12 14621  wfrlem15 14624  frr3g 14633  frrlem1 14634  frrlem4 14637  frrlem11 14646  sltval 14654  sltval2 14662  sltres 14670  axdense 14696  nocvxminlem 14697  axfelem9 14707  axfelem10 14708  axfelem12 14710  axfelem18 14716  axfelem22 14720  brtxp 14752  dfbigcup2 14760  elfix 14764  dffix2 14766  elfuns 14774  dfoprab4spop 15047  splint 15060  ficli 15063  vxveqv 15067  ac5g 15098  injrec 15173  injrec2 15178  surjsec2 15179  cmpbvb 15211  repcpwti 15242  cbicplem 15247  prjmapcp2 15254  iserzmulc1b 15267  islatalg 15270  cur1val 15285  preotr2 15315  supdef 15343  inposet 15359  dutos1 15365  isdir2 15379  dffprod 15409  ridlideq 15430  rzrlzreq 15431  isppm 15450  symgfo 15465  curgrpact 15470  fprodsub 15477  cmprtr 15494  cmpltr 15506  ununr 15522  vecval1b 15547  vecval3b 15548  svs2 15582  vri 15587  osneisi 15632  hmeogrp 15649  intopcoaconb 15662  intopcoaconc 15663  qusp 15671  topgele 15673  ptincpw 15676  intcont 15679  usptoplem 15682  istopx 15683  prtoptop 15684  usptop 15685  prcnt 15686  cnfilca 15693  rcfpfillem3 15696  exopcopn 15721  prdnei 15722  limptlimpr2lem1 15723  limptlimpr2lem2 15724  bwt2 15738  clindistop 15740  topsinind 15745  grphm 15774  altretoplem2 15787  altretop 15788  cntrsetlem 15791  trnij 15807  cnvtr 15808  letri31 15811  supnuf 15835  supexr 15837  ismgra 15851  isalg 15862  algi 15868  isded 15877  dedi 15878  idosd 15885  iscat 15895  cati 15896  cmpasso 15914  dualded 15926  dualcat2 15927  ishomd 15933  ismona 15952  ismonb 15953  imonclem 15956  isepia 15962  isepib 15963  iepiclem 15966  cinvlem1 15970  cinvlem2 15971  cinvlem3 15972  isfuna 15976  isfunb 15977  issubcat 15987  issubcata 15988  issubcatb 15989  infemb 16001  tarval 16022  tarvalg 16023  tarval1 16024  tarval1g 16025  tclinf 16051  bpmp 16061  btmp 16062  isplibg0 16117  isplibg2 16121  isplibg4b 16127  isplibg 16129  trer 16185  finminlem 16191  elfiun 16193  fictb 16195  ordisoOLD 16198  ordtypelem1OLD 16199  ordtypelem6OLD 16204  ordtypeOLD 16206  hartog 16208  opncldf1 16226  opncldf2 16227  opncldf3 16228  compsublem 16254  compsub 16255  hscptsscld 16258  compfipin0 16260  alexsublem1 16261  alexsublem2 16262  alexsublem3 16263  alexsublem4 16264  connsub 16267  cnconn 16268  reconnlem1 16270  2ndcsb 16300  2ndc1stc 16301  2ndcctbss 16302  isfne 16304  isfne3 16306  isref 16312  fness 16315  fneref 16317  fnessref 16327  refssfne 16328  comppfsc 16341  neibastop1 16342  neibastop2lem1 16343  neibastop2lem2 16344  neibastop2lem3 16345  neibastop2lem4 16346  neibastop2 16347  neibastop3 16348  topmtcl 16349  topmeet 16350  topjoin 16351  fnemeet1 16352  fnemeet2 16353  fnejoin1 16354  ist1-2 16366  ist1-3 16367  neifg 16383  supfil 16384  filfinnfr 16385  isufil2 16389  ufilmax 16392  filssufillem 16394  filssufil 16395  ufileu 16397  fixufil 16400  ufinffr 16402  ufilen 16403  filcon 16404  limfilcf 16411  cnpfillim 16413  rnelfm 16417  sfcls 16428  fcluscf 16436  flimfnfcls 16439  fcluscnplem 16441  fcluscnp 16442  fclusff 16447  sfclusf 16448  tailf 16457  istail 16458  tailuni 16462  tailfb 16463  filnetlem1 16464  filnetlem2 16465  filnetlem3 16466  filnetlem4 16467  filnetlem5 16468  filnet 16469  unirep 16488  ralrabOLD 16494  inpreimaOLD 16506  opabex3OLD 16525  oprabvalg 16530  oprabval2a 16531  cbvoprab2 16532  upixp 16553  eropreu 16557  eroprv 16558  fimaxgOLD 16571  acdcg 16574  acdc3g 16575  acdc5g 16576  indexdom 16578  inficl 16581  sdclem2 16634  sdc 16635  fdc 16636  fdc1 16637  fsumltisumi 16647  fsumltisum 16648  iserzshft2 16653  fsumlt1 16655  blhalf 16670  mettrifi 16671  caures 16676  metdcn 16677  iccss2 16680  icoopnst 16700  iocopnst 16701  cncfco 16711  haustlmu 16730  txcnoprab 16735  cnopropabco 16741  cnoproprabco 16743  txmet 16749  istotbnd 16757  sstotbnd 16760  totbndss 16761  ismtyval 16771  isismty 16772  ismtyhmeolem 16774  ismtyres 16778  heiborlem1 16779  heiborlem18 16796  heiborlem28 16806  heiborlem30 16808  heiborlem32 16810  heiborlem35 16813  heiborlem36 16814  heiborlem42 16820  bfplem3 16824  bfplem8 16829  bfplem11 16832  bfp 16833  recms 16834  rrnval 16837  rrnmet 16840  rrncms 16843  rrntotbndlem1 16844  rrntotbnd 16846  rrnheibor 16847  reheibor 16849  exidcl 16853  exidreslem 16854  exidres 16855  exidresid 16856  isgrpda 16857  isablda 16859  ghomco 16864  phtpyfval 16870  phtpyval 16871  isphtpy 16872  phtpycom 16874  phtpyco 16880  phtpcval 16882  isphtpc 16883  phtpcer 16886  pcofval 16896  pcoval 16897  pcoloopf 16903  pcohtpy 16907  pi1bval 16912  elpi1i 16914  pi1bvalqs 16915  pi1fval 16916  pi1f 16917  pi1val 16918  isringd 16921  divrngcl 16934  rnghomval 16942  isrnghom 16943  isriscg 16962  iscringd 16971  idlval 16985  isidl 16986  0idl 16997  keridl 17004  pridlval 17005  ispridl 17006  maxidlval 17011  ismaxidl 17012  smprngpr 17024  igenval 17033  prnc 17039  ispridlc 17042  isdmn3 17046  ertr2 17081  prtlem10 17089  prtlem13 17095  prtlem15 17105  prter1 17106  prter3 17110  ishgrag 17115  hgralem 17116  ispgrag 17125  sbiota1 17223  cbvrexcsfOLD 17236  cbvreucsfOLD 17237  cbvrabcsfOLD 17238  smoisoOLD 17275  lubunNEW 17565  isopos 17576  opltcon3b 17598  omlfh3 17652  cvrfval 17660  cvrval 17661  cvrnbtwn 17663  cvrcon3b 17668  cvrnbtwn4 17670  cvrcmp2 17675  isatl 17696  iscvlat 17720  cvlexch1 17725  ishlat1 17748  glbcon 17770  hlsuprexch 17775  hlateq 17794  hlrelat 17797  hlrelat2 17798  cvrexchlem 17814  cvrat4 17839  3dim0 17853  3dim2 17864  2dim 17866  ps-2 17874  issrng 17888  islvec 17900  isphil 17907  csubspset 17920  iscsubsp 17921  islln3 17942  llni2 17944  llnexatOLD 17953  islpln5 17966  lplnexlln 17996  lvoli3 18009  islvol5 18011  lvoli2 18013  4atlem3 18028  4atlem12 18044  islinei 18173  psubspset 18177  ispsubsp 18178  pointpsub 18183  pmap11 18194  isline4 18209  lnatex 18211  pmapjoin 18284  pmapjat1 18285  psubclset 18350  ispsubcl 18351  ispsubcl2 18361  lhprelat3 18435  lautset 18437  islaut 18438  lautlt 18445  lautcvr 18446  pautset 18452  ispaut 18453  ltrnfset 18470  ltrnset 18471  ltrnatb 18488  4atexlemex2 18541  cdleme0ex1 18592  cdleme0nex 18661  cdleme25b 18726  cdleme25cv 18730  cdleme29b 18748  cdlemefrs29bpre0 18770  cdlemefrs32fva 18774  cdlemefr32sn2aw 18778  cdlemefs32sn1aw 18788  cdleme32fvawOLD 18814  cdleme32fvaw 18815  cdleme40vOLD 18846  cdleme40v 18848  cdleme42b 18857  cdleme46f2g1 18875  cdleme48gfv 18922  cdleme50eq 18926  cdlemg1fvawlem 18952  cdlemgfvawOLD 18964

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 220  df-an 339

Copyright terms: Public domain