Theorem bibi12d 632

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

Hypotheses

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

Assertion

Ref	Expression
bibi12d	|- (ph -> ((ps <-> th) <-> (ch <-> ta)))

Proof of Theorem bibi12d

Step	Hyp	Ref	Expression
1		bi12d.1	. . 3 |- (ph -> (ps <-> ch))
2	1	bibi1d 622	. 2 |- (ph -> ((ps <-> th) <-> (ch <-> th)))
3		bi12d.2	. . 3 |- (ph -> (th <-> ta))
4	3	bibi2d 621	. 2 |- (ph -> ((ch <-> th) <-> (ch <-> ta)))
5	2, 4	bitrd 531	1 |- (ph -> ((ps <-> th) <-> (ch <-> ta)))

Syntax hints:   -> wi 3   <-> wb 144

This theorem is referenced by:  bi2bian9 637  cleqf 1603  vtoclb 1891  vtoclbg 1894  ceqsexg 1933  elabgf 1944  reu3 1977  ru 1984  sbcbidig 2021  sbceqdig 2063  unineq 2307  elpwg 2462  prssg 2537  elintg 2608  axrep4 2771  nalset 2786  opthgg 2865  so 2943  reuuni2f 3107  orduninsuc 3197  opelco2g 3380  resieq 3463  elimasng 3519  eliniseg 3521  asymref2 3532  cnvopab 3537  fnbrfvb 3864  funbrfvbg 3868  eqfnfv 3909  eqfnfv2 3911  fressnfv 3952  isorel 4008  isocnv 4010  isotr 4011  isotrALT 4012  caoprord 4117  erth 4422  ecopoprsym 4451  pw2en 4587  nneneq 4659  rankr1g 4821  r1pw 4832  karden 4872  aceq0 4876  zfac 4891  axextnd 5097  axrepndlem1 5098  axrepndlem2 5099  axrepnd 5100  axacndlem5 5117  zfcndrep 5120  zfcndac 5125  ltpiord 5169  ltsopq 5229  ltapq 5230  ltmpq 5231  ltsosr 5357  ltasr 5363  ltsor 5415  pre-axltadd 5443  addcan 5506  subaddi 5525  subadd 5529  neg11 5563  ltadd1 5777  leadd1 5779  ltsubadd 5781  lesubadd 5783  ltneg 5809  leneg 5811  lesub0 5832  mulcant2i 5843  mul0or 5848  divmuli 5857  divmulzi 5858  divmul 5859  div11 5904  rec11i 5917  redivcli 5938  eqneg 5945  ltmul1 5970  ltdiv1 5993  ltdiv1OLD 5994  ltmuldiv 6007  ltmuldivOLD 6008  ltreci 6024  ltrec 6029  lerec 6030  lt2msq 6031  le2msq 6048  nnsub 6103  halfpos 6182  nn0sub 6329  zltp1le 6349  zextle 6360  zextlt 6361  nneo 6369  sq11 6826  sqeqor 6846  discrlem2 6858  nn0opth2 6869  sqrlem12 6885  sqrle 6914  sqr00 6915  sqr2irrlem5 6929  cru 6939  replim 6962  cjreb 7001  abs00 7055  abslt 7083  absle 7084  absgt0 7096  climfnn 7295  iserzshft2i 7310  reef11 7617  reefiso 7636  meteq0 8022  cnid 8368  mulid 8373  nmlno0i 8709  nmlno0 8710  blocn 8722  cosh111 8989  logltb 9048  hvsubeq0 9210  hvaddcan 9212  hvsubadd 9220  normsub0 9279  hilid 9304  projlem1 9462  pjthlem9 9503  pjoc1 9543  pjoc2 9548  shlub 9630  chne0 9693  chsscon3 9699  chlejb1 9711  chnle 9713  h1de2ci 9755  elspansn 9765  elspansn2 9766  cmbr3 9827  cmcm 9833  cmcm3 9834  pjch1 9893  pjch 9917  pj11 9937  pjnel 9949  eigorth 10044  nmlnop0 10202  lnopeq 10213  lnopcon 10243  lnfncon 10270  pjdifnormi 10375  chrelat2 10578  cvexch 10582  mdsym 10621  abs2sqlet 10659  abs2sqltt 10660  on1el3 10962  homcard 11045  issubsplem1 11058  issubspt 11059  cmppfd 11199  ishomd 11245  cbvsbc 11398  inficlALT 11424  cnconn 11503  neibastop3 11585  erthdmg 11824  add20 11858  iserzshft2 11892

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 145  df-an 223

Copyright terms: Public domain