Theorem anbi12d 476

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

Hypotheses

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

Assertion

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

Proof of Theorem anbi12d

Step	Hyp	Ref	Expression
1		bi2d.1	. . 3 |- (ph -> (ps <-> ch))
2	1	anbi1d 469	. 2 |- (ph -> ((ps /\ th) <-> (ch /\ th)))
3		bi2d.2	. . 3 |- (ph -> (th <-> ta ))
4	3	anbi2d 468	. 2 |- (ph -> ((ch /\ th) <-> (ch /\ ta )))
5	2, 4	bitrd 406	1 |- (ph -> ((ps /\ th) <-> (ch /\ ta )))

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196

This theorem is referenced by:  bi3and 636  mopick 1054  axun 1081  axac 1085  clelab 1187  cbvrex 1332  cbvreuv 1335  reu2 1338  gencbvex 1372  rcla4ev 1403  eqvincf 1408  ceqsrexv 1413  elrabf 1421  cbvrab 1425  sbcan 1461  nalset 1482  eldif 1496  psseq1 1559  psseq2 1560  ssconb 1598  elin 1635  nnullss 1880  exss 1881  elunii 1924  eluniab 1926  unipw 1960  opabid 2099  cbvopab 2104  cbvopab1 2106  cbvopab1s 2107  cbvopab1v 2108  cbvopab2v 2109  poeq1 2130  pocl 2132  soeq1 2141  supeq1 2155  supmo 2156  supub 2160  suplub 2161  supsn 2168  fri 2170  frc 2172  weeq1 2189  weeq2 2190  ordeq 2206  onminex 2275  limsuc 2361  elom 2375  elomg 2376  vtoclr 2449  brinxp 2466  opbrop 2472  cbvop 2473  elxp4 2640  elxp5 2641  fununi 2705  funcnvuni 2706  fneq1 2718  2elresin 2733  feq1 2748  fcoi2 2766  f1eq1 2776  foeq1 2784  f1oeq1 2795  f1oeq2 2796  f1oeq3 2797  ffoss 2820  fv3 2839  tz6.12f 2844  fnopabfv 2858  fvopab3 2868  fvopab3ig 2869  isoeq1 2925  isoeq4 2928  isomin 2937  isoini 2938  isofrlem 2939  isowe 2941  f1oweOLD 2944  tfrlem1 2949  tfrlem3 2951  tfrlem5 2953  tfrlem12 2960  tz7.44-2 2967  tz7.44-3 2968  rdglem2 2976  cbvoprab12 3028  oprabval 3047  oprabvalig 3048  oprabval4g 3053  caoprmo 3084  ertr 3211  ecelqsi 3229  brecop 3242  ecopoprtrn 3247  th3qlem1 3250  th3qlem2 3251  th3q 3253  mapsnen 3334  xpsnen 3339  endisj 3341  pw2en 3348  sbthlem2 3350  sbth 3359  php2 3410  nnsdomo 3417  unfilem1 3438  fiint 3445  en2lp 3453  inf0 3457  inf4 3473  dfom3 3477  rankr1g 3519  r1pwcl 3530  karden 3551  aceq1 3552  aceq0 3553  aceq2 3554  aceq3lem 3555  aceq3 3556  aceq4 3557  aceq5lem1 3558  aceq5lem2 3559  aceq5lem3 3560  aceq5lem4 3561  aceq5 3563  aceq6a 3564  aceq6b 3565  ac7g 3570  ac5 3573  ac6lem 3575  kmlem1 3580  kmlem2 3581  kmlem4 3583  kmlem14 3593  zornlem1 3603  zornlem7 3609  zorn 3611  cardsdom 3643  alephnbtwn2 3675  aleph11 3684  cflem 3700  cfval 3701  cflecard 3707  cfsuc 3709  axrepndlem2 3739  axunnd 3742  axregndlem2 3749  axinfndlem1 3751  axacndlem5 3757  axacnd 3758  zfcndun 3761  zfcndac 3765  ltsopi 3810  indpi 3828  ltsopq 3869  ltbtwnpq 3878  elnp 3886  prcdpq 3891  genpv 3896  genpprecl 3898  genpnmax 3904  ltprord 3928  ltsopr 3930  ltexprlem4 3939  ltexprlem7 3942  prlem936 3949  reclem1pr 3950  reclem3pr 3952  suppr 3957  ltsosr 3997  negexsr 4005  recexsr 4010  suppsr 4016  suppsr3 4018  supsrlem5 4023  supsrlem6 4024  ltresr 4052  supre 4054  ltsor 4055  axnegex 4078  axrecex 4079  axrnegex 4080  axrrecex 4081  axcnre 4087  dividt 4256  recrect 4260  letri3t 4283  lesub0t 4374  posex 4422  peano5nn 4424  nnind 4434  nn2get 4438  nominpos 4509  sup2 4510  sup3 4511  nnunb 4520  zltp1let 4597  uzind 4603  nnwof 4609  zmax 4618  rebtwnz 4620  flvalt 4623  flleltt 4625  qbtwnre 4650  sqr0 4730  sqrlem4 4734  sqrlem24 4754  sqrgt0i 4755  sqrlem26 4756  sqr2irrlem2 4778  absltt 4857  abs3lemt 4865  clim 4877  clim2 4881  climuni 4884  ruclem4 4888  ruclem12 4896  ruclem29 4913  ruclem36 4920  infxpidmlem2 4934  infxpidmlem3 4935  infxpidmlem8 4940  infmap2lem1 4951  normlem7t 5072  norm3lemt 5097  hcauchy 5103  hlim 5108  hlim2 5112  sh 5116  closedsub 5128  chlim 5139  hlimuni 5144  ch2 5149  ocsh 5164  ocin 5177  projlem7 5199  projlem17 5209  projlem26 5218  projlem28 5220  pjthut 5243  pjmvalt 5245  omls 5251  shintclt 5295  chintclt 5297  shlubt 5355  chpsscon3t 5420  cmbrt 5494  pjoml5 5498  spansncvt 5543  pjrn 5587  stelt 5671  jp 5703  cvbrt 5714  cvcon3t 5716  cvnbtwnt 5718  mdbr 5726  elat2 5739  chrelat 5757  chrelat2 5758  cvexchlem 5759  atcvat4 5775  mdsymlem2 5777  mdsymlem8 5783

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org