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 ⊢ (𝜒 → (𝜑 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  syl5ibrcom  157  biimprd  158  nbn2  709  anifpdc  999  limelon  4546  eldifpw  4625  ssonuni  4637  onsucuni2  4713  peano2  4744  limom  4763  elrnmpt1  5035  cnveqb  5246  cnveq0  5247  relcoi1  5322  f1ssf1  5674  ndmfvg  5729  ffvresb  5874  caovord3d  6263  poxp  6472  nnm0r  6756  nnacl  6757  nnacom  6761  nnaass  6762  nndi  6763  nnmass  6764  nnmsucr  6765  nnmcom  6766  brecop  6903  ecopovtrn  6910  ecopovtrng  6913  elpm2r  6944  map0g  6973  fundmen  7099  dom1o  7121  mapxpen  7153  mapunen  7156  phpm  7172  f1vrnfibi  7264  elfir  7313  mulcmpblnq  7742  ordpipqqs  7748  mulcmpblnq0  7818  genpprecll  7888  genppreclu  7889  addcmpblnr  8113  ax1rid  8251  axpre-mulgt0  8261  cnegexlem1  8509  msqge0  8953  mulge0  8956  ltleap  8969  nnmulcl  9335  nnsub  9353  elnn0z  9669  ztri3or0  9698  nneoor  9760  uz11  9962  xltnegi  10255  frec2uzuzd  10861  seq3fveq2  10934  seqfveq2g  10936  seq3shft2  10940  seqshft2g  10941  seq3split  10947  seqsplitg  10948  seq3caopr3  10950  seqcaopr3g  10951  seqf1oglem2a  10977  seq3id2  10985  seq3homo  10986  seqhomog  10989  m1expcl2  11020  expadd  11040  expmul  11043  faclbnd  11202  hashfzp1  11288  hashmap  11291  hashfacen  11307  hashf1lem2  11309  hashf1  11310  seq3coll  11317  wrdsymb0  11360  len0nnbi  11362  wrd2ind  11518  pfxccatin12lem2c  11525  pfxccatin12lem2  11526  swrdccatin1d  11538  caucvgrelemcau  11769  recan  11899  rexanre  12010  fsumiun  12270  efexp  12475  dvdstr  12621  alzdvds  12647  zob  12684  bitsinv1  12755  gcdmultiplez  12824  dvdssq  12834  cncongr2  12908  prmdiveq  13044  pythagtriplem2  13075  pcexp  13118  elrestr  13661  ptex  13678  xpsff1o  13730  dfgrp3me  13965  mulgneg2  14019  mulgnnass  14020  mhmmulg  14026  gsum2dfilem2  14273  rngpropd  14362  ringadd2  14440  mulgass2  14471  opprrngbg  14493  opprsubrngg  14629  subrngpropd  14634  subrgpropd  14671  rhmpropd  14672  lmodprop2d  14795  cnfldmulg  15023  cnfldexp  15024  assapropd  15124  restopn2  15421  txcn  15513  txlm  15517  isxms2  15690  rpcxpmul2  16158  chtqub  16308  gausslemma2dlem0i  16393  incistruhgr  16548  upgredg2vtx  16606  upgredgpr  16607  uhgr2edg  16664  wlkres  16837  clwwlknonex2  16897  eupth2lem3lem6fi  16929  bj-om  17180  bj-inf2vnlem2  17214  bj-inf2vn  17217  bj-inf2vn2  17218