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  705  anifpdc  995  limelon  4519  eldifpw  4597  ssonuni  4609  onsucuni2  4685  peano2  4716  limom  4735  elrnmpt1  5007  cnveqb  5217  cnveq0  5218  relcoi1  5293  f1ssf1  5645  ndmfvg  5700  ffvresb  5839  caovord3d  6224  poxp  6427  nnm0r  6711  nnacl  6712  nnacom  6716  nnaass  6717  nndi  6718  nnmass  6719  nnmsucr  6720  nnmcom  6721  brecop  6858  ecopovtrn  6865  ecopovtrng  6868  elpm2r  6899  map0g  6921  fundmen  7046  dom1o  7068  mapxpen  7100  mapunen  7103  phpm  7119  f1vrnfibi  7211  elfir  7259  mulcmpblnq  7682  ordpipqqs  7688  mulcmpblnq0  7758  genpprecll  7828  genppreclu  7829  addcmpblnr  8053  ax1rid  8191  axpre-mulgt0  8201  cnegexlem1  8447  msqge0  8889  mulge0  8892  ltleap  8905  nnmulcl  9257  nnsub  9275  elnn0z  9589  ztri3or0  9618  nneoor  9679  uz11  9876  xltnegi  10167  frec2uzuzd  10763  seq3fveq2  10836  seqfveq2g  10838  seq3shft2  10842  seqshft2g  10843  seq3split  10849  seqsplitg  10850  seq3caopr3  10852  seqcaopr3g  10853  seqf1oglem2a  10879  seq3id2  10887  seq3homo  10888  seqhomog  10891  m1expcl2  10922  expadd  10942  expmul  10945  faclbnd  11102  hashfzp1  11187  hashfacen  11204  seq3coll  11210  wrdsymb0  11253  len0nnbi  11255  wrd2ind  11411  pfxccatin12lem2c  11418  pfxccatin12lem2  11419  swrdccatin1d  11431  caucvgrelemcau  11661  recan  11790  rexanre  11901  fsumiun  12159  efexp  12364  dvdstr  12510  alzdvds  12536  zob  12573  bitsinv1  12644  gcdmultiplez  12713  dvdssq  12723  cncongr2  12797  prmdiveq  12929  pythagtriplem2  12960  pcexp  13003  elrestr  13452  ptex  13469  xpsff1o  13554  dfgrp3me  13805  mulgneg2  13865  mulgnnass  13866  mhmmulg  13872  rngpropd  14091  ringadd2  14163  mulgass2  14194  opprrngbg  14214  opprsubrngg  14348  subrngpropd  14353  subrgpropd  14390  rhmpropd  14391  lmodprop2d  14488  cnfldmulg  14716  cnfldexp  14717  restopn2  15040  txcn  15132  txlm  15136  isxms2  15309  rpcxpmul2  15770  gausslemma2dlem0i  15922  incistruhgr  16077  upgredg2vtx  16135  upgredgpr  16136  uhgr2edg  16193  wlkres  16366  clwwlknonex2  16426  eupth2lem3lem6fi  16458  bj-om  16699  bj-inf2vnlem2  16733  bj-inf2vn  16736  bj-inf2vn2  16737