Theorem bitrns-P3.33c.RC 303

Description: Inference Form of bitrns-P3.33c 302. †

Hypotheses

Ref	Expression
bitrns-P3.33c.RC.1	⊢ (𝜑 ↔ 𝜓)
bitrns-P3.33c.RC.2	⊢ (𝜓 ↔ 𝜒)

Assertion

Ref	Expression
bitrns-P3.33c.RC	⊢ (𝜑 ↔ 𝜒)

Proof of Theorem bitrns-P3.33c.RC

Step	Hyp	Ref	Expression
1		bitrns-P3.33c.RC.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
2	1	ndtruei-P3.17 182	. . 3 ⊢ (⊤ → (𝜑 ↔ 𝜓))
3		bitrns-P3.33c.RC.2	. . . 4 ⊢ (𝜓 ↔ 𝜒)
4	3	ndtruei-P3.17 182	. . 3 ⊢ (⊤ → (𝜓 ↔ 𝜒))
5	2, 4	bitrns-P3.33c 302	. 2 ⊢ (⊤ → (𝜑 ↔ 𝜒))
6	5	ndtruee-P3.18 183	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wff-bi 104  ⊤wff-true 153

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14

This theorem depends on definitions:  df-bi-D2.1 107  df-and-D2.2 133  df-true-D2.4 155

This theorem is referenced by:  oroverbi-P4.28-L3  468  imoverbi-P4.30-L2  478  lemma-L4.5  484  imasand-P4.33a  489  biasandor-P4.34a  491  allnegex-P5  597  exnegall-P5  598  allasex-P5  599  lemma-L5.01a  600  lemma-L5.03a  666  example-E5.04a  675  solvedsub-P6a  711  dfpsubv-P6  717  isubtopsubv-P6  727  lemma-L6.03a  728  isubtopsub-P6  729  qcexandr-P6  761  qcexandl-P6  762  lemma-L6.08a  773  dfpsubalt-P6  774  psubneg-P6-L1  787  psubneg-P6  788  psuband-P6  792  psubex2v-P6  797  psuball2-P6  798  psubex2-P6  799  psubsplitelof-P6  801  psubid-P7  940  dfnfreeint-P7  969  exnegall-P7  1046  allasex-P7  1048