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  698  limelon  4435  eldifpw  4513  ssonuni  4525  onsucuni2  4601  peano2  4632  limom  4651  elrnmpt1  4918  cnveqb  5126  cnveq0  5127  relcoi1  5202  ndmfvg  5592  ffvresb  5728  caovord3d  6098  poxp  6299  nnm0r  6546  nnacl  6547  nnacom  6551  nnaass  6552  nndi  6553  nnmass  6554  nnmsucr  6555  nnmcom  6556  brecop  6693  ecopovtrn  6700  ecopovtrng  6703  elpm2r  6734  map0g  6756  fundmen  6874  mapxpen  6918  phpm  6935  f1vrnfibi  7020  elfir  7048  mulcmpblnq  7454  ordpipqqs  7460  mulcmpblnq0  7530  genpprecll  7600  genppreclu  7601  addcmpblnr  7825  ax1rid  7963  axpre-mulgt0  7973  cnegexlem1  8220  msqge0  8662  mulge0  8665  ltleap  8678  nnmulcl  9030  nnsub  9048  elnn0z  9358  ztri3or0  9387  nneoor  9447  uz11  9643  xltnegi  9929  frec2uzuzd  10513  seq3fveq2  10586  seqfveq2g  10588  seq3shft2  10592  seqshft2g  10593  seq3split  10599  seqsplitg  10600  seq3caopr3  10602  seqcaopr3g  10603  seqf1oglem2a  10629  seq3id2  10637  seq3homo  10638  seqhomog  10641  m1expcl2  10672  expadd  10692  expmul  10695  faclbnd  10852  hashfzp1  10935  hashfacen  10947  seq3coll  10953  wrdsymb0  10986  len0nnbi  10988  caucvgrelemcau  11164  recan  11293  rexanre  11404  fsumiun  11661  efexp  11866  dvdstr  12012  alzdvds  12038  zob  12075  bitsinv1  12146  gcdmultiplez  12215  dvdssq  12225  cncongr2  12299  prmdiveq  12431  pythagtriplem2  12462  pcexp  12505  elrestr  12951  ptex  12968  xpsff1o  13053  dfgrp3me  13304  mulgneg2  13364  mulgnnass  13365  mhmmulg  13371  rngpropd  13589  ringadd2  13661  mulgass2  13692  opprrngbg  13712  opprsubrngg  13845  subrngpropd  13850  subrgpropd  13887  rhmpropd  13888  lmodprop2d  13982  cnfldmulg  14210  cnfldexp  14211  restopn2  14527  txcn  14619  txlm  14623  isxms2  14796  rpcxpmul2  15257  gausslemma2dlem0i  15406  bj-om  15691  bj-inf2vnlem2  15725  bj-inf2vn  15728  bj-inf2vn2  15729