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  699  limelon  4451  eldifpw  4529  ssonuni  4541  onsucuni2  4617  peano2  4648  limom  4667  elrnmpt1  4935  cnveqb  5144  cnveq0  5145  relcoi1  5220  ndmfvg  5617  ffvresb  5753  caovord3d  6127  poxp  6328  nnm0r  6575  nnacl  6576  nnacom  6580  nnaass  6581  nndi  6582  nnmass  6583  nnmsucr  6584  nnmcom  6585  brecop  6722  ecopovtrn  6729  ecopovtrng  6732  elpm2r  6763  map0g  6785  fundmen  6909  mapxpen  6957  phpm  6974  f1vrnfibi  7059  elfir  7087  mulcmpblnq  7494  ordpipqqs  7500  mulcmpblnq0  7570  genpprecll  7640  genppreclu  7641  addcmpblnr  7865  ax1rid  8003  axpre-mulgt0  8013  cnegexlem1  8260  msqge0  8702  mulge0  8705  ltleap  8718  nnmulcl  9070  nnsub  9088  elnn0z  9398  ztri3or0  9427  nneoor  9488  uz11  9684  xltnegi  9970  frec2uzuzd  10560  seq3fveq2  10633  seqfveq2g  10635  seq3shft2  10639  seqshft2g  10640  seq3split  10646  seqsplitg  10647  seq3caopr3  10649  seqcaopr3g  10650  seqf1oglem2a  10676  seq3id2  10684  seq3homo  10685  seqhomog  10688  m1expcl2  10719  expadd  10739  expmul  10742  faclbnd  10899  hashfzp1  10982  hashfacen  10994  seq3coll  11000  wrdsymb0  11039  len0nnbi  11041  caucvgrelemcau  11341  recan  11470  rexanre  11581  fsumiun  11838  efexp  12043  dvdstr  12189  alzdvds  12215  zob  12252  bitsinv1  12323  gcdmultiplez  12392  dvdssq  12402  cncongr2  12476  prmdiveq  12608  pythagtriplem2  12639  pcexp  12682  elrestr  13129  ptex  13146  xpsff1o  13231  dfgrp3me  13482  mulgneg2  13542  mulgnnass  13543  mhmmulg  13549  rngpropd  13767  ringadd2  13839  mulgass2  13870  opprrngbg  13890  opprsubrngg  14023  subrngpropd  14028  subrgpropd  14065  rhmpropd  14066  lmodprop2d  14160  cnfldmulg  14388  cnfldexp  14389  restopn2  14705  txcn  14797  txlm  14801  isxms2  14974  rpcxpmul2  15435  gausslemma2dlem0i  15584  incistruhgr  15736  bj-om  15987  bj-inf2vnlem2  16021  bj-inf2vn  16024  bj-inf2vn2  16025  dom1o  16043