Theorem imbitrrid 156

Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.) (Revised by NM, 22-Sep-2013.)

Hypotheses

Ref	Expression
imbitrrid.1	⊢ (𝜑 → 𝜃)
imbitrrid.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
imbitrrid	⊢ (𝜒 → (𝜑 → 𝜓))

Proof of Theorem imbitrrid

Step	Hyp	Ref	Expression
1		imbitrrid.1	. 2 ⊢ (𝜑 → 𝜃)
2		imbitrrid.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	2	bicomd 141	. 2 ⊢ (𝜒 → (𝜃 ↔ 𝜓))
4	1, 3	imbitrid 154	1 ⊢ (𝜒 → (𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  syl5ibrcom  157  biimprd  158  nbn2  697  limelon  4401  eldifpw  4479  ssonuni  4489  onsucuni2  4565  peano2  4596  limom  4615  elrnmpt1  4880  cnveqb  5086  cnveq0  5087  relcoi1  5162  ndmfvg  5548  ffvresb  5681  caovord3d  6047  poxp  6235  nnm0r  6482  nnacl  6483  nnacom  6487  nnaass  6488  nndi  6489  nnmass  6490  nnmsucr  6491  nnmcom  6492  brecop  6627  ecopovtrn  6634  ecopovtrng  6637  elpm2r  6668  map0g  6690  fundmen  6808  mapxpen  6850  phpm  6867  f1vrnfibi  6946  elfir  6974  mulcmpblnq  7369  ordpipqqs  7375  mulcmpblnq0  7445  genpprecll  7515  genppreclu  7516  addcmpblnr  7740  ax1rid  7878  axpre-mulgt0  7888  cnegexlem1  8134  msqge0  8575  mulge0  8578  ltleap  8591  nnmulcl  8942  nnsub  8960  elnn0z  9268  ztri3or0  9297  nneoor  9357  uz11  9552  xltnegi  9837  frec2uzuzd  10404  seq3fveq2  10471  seq3shft2  10475  seq3split  10481  seq3caopr3  10483  seq3id2  10511  seq3homo  10512  m1expcl2  10544  expadd  10564  expmul  10567  faclbnd  10723  hashfzp1  10806  hashfacen  10818  seq3coll  10824  caucvgrelemcau  10991  recan  11120  rexanre  11231  fsumiun  11487  efexp  11692  dvdstr  11837  alzdvds  11862  zob  11898  gcdmultiplez  12024  dvdssq  12034  cncongr2  12106  prmdiveq  12238  pythagtriplem2  12268  pcexp  12311  elrestr  12701  ptex  12718  xpsff1o  12773  dfgrp3me  12975  mulgneg2  13022  mulgnnass  13023  mhmmulg  13029  ringadd2  13215  mulgass2  13240  subrgpropd  13374  lmodprop2d  13443  cnfldmulg  13555  cnfldexp  13556  restopn2  13768  txcn  13860  txlm  13864  isxms2  14037  bj-om  14774  bj-inf2vnlem2  14808  bj-inf2vn  14811  bj-inf2vn2  14812