Theorem bitr4d 409

Description: Deduction form of bitr4 154.

Hypotheses

Ref	Expression
bitr4d.1	⊢ (φ → (ψ ↔ χ))
bitr4d.2	⊢ (φ → (θ ↔ χ))

Assertion

Ref	Expression
bitr4d	⊢ (φ → (ψ ↔ θ))

Proof of Theorem bitr4d

Step	Hyp	Ref	Expression
1		bitr4d.1	. 2 ⊢ (φ → (ψ ↔ χ))
2		bitr4d.2	. . 3 ⊢ (φ → (θ ↔ χ))
3	2	bicomd 399	. 2 ⊢ (φ → (χ ↔ θ))
4	1, 3	bitrd 406	1 ⊢ (φ → (ψ ↔ θ))

Syntax hints:   → wi 2   ↔ wb 127

This theorem is referenced by:  3bitr4d 424  ceqsrexv 1413  sbc19.21g 1470  reuhyp 1581  ordtri4 2235  ordsssuc 2310  opbrop 2472  dmsnop 2547  iss 2599  fnopabfv 2858  dmfco 2864  fvco 2865  f1fv 2916  isoini 2938  oprabval 3047  caoprord3 3072  oe1m 3147  oawordri 3152  oalimcl 3162  brecop 3242  ecopoprsym 3246  xpdom2 3345  mapxpen 3390  r1pw 3529  r1pwcl 3530  cardnn 3631  ltsopq 3869  ltapq 3870  ltmpq 3871  ltexpq2 3875  genpass 3906  ltprord 3928  prlem936a 3947  ltsosr 3997  ltasr 4003  divneq0bt 4230  leltt 4278  letri3t 4283  lesub1t 4352  ltsubadd2t 4354  lesubadd2t 4356  ltsub23t 4359  ltsubpost 4364  lerec 4411  nnltp1let 4449  nn0ltp1let 4556  nn0leltp1t 4557  zleltp1t 4598  qbtwnre 4650  om2uzlt 4654  le2sqet 4707  replimt 4798  clim2 4881  xpnnen 4927  znnen 4930  normgt0t 5078  hlim2 5112  shselt 5280  cmbrt 5494  pjnormss 5638  pjelt 5668  jplem1 5701  cvbrt 5714  mdbr 5726

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