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  4544  eldifpw  4623  ssonuni  4635  onsucuni2  4711  peano2  4742  limom  4761  elrnmpt1  5033  cnveqb  5243  cnveq0  5244  relcoi1  5319  f1ssf1  5671  ndmfvg  5726  ffvresb  5871  caovord3d  6260  poxp  6468  nnm0r  6752  nnacl  6753  nnacom  6757  nnaass  6758  nndi  6759  nnmass  6760  nnmsucr  6761  nnmcom  6762  brecop  6899  ecopovtrn  6906  ecopovtrng  6909  elpm2r  6940  map0g  6969  fundmen  7094  dom1o  7116  mapxpen  7148  mapunen  7151  phpm  7167  f1vrnfibi  7259  elfir  7307  mulcmpblnq  7735  ordpipqqs  7741  mulcmpblnq0  7811  genpprecll  7881  genppreclu  7882  addcmpblnr  8106  ax1rid  8244  axpre-mulgt0  8254  cnegexlem1  8501  msqge0  8945  mulge0  8948  ltleap  8961  nnmulcl  9326  nnsub  9344  elnn0z  9659  ztri3or0  9688  nneoor  9750  uz11  9947  xltnegi  10239  frec2uzuzd  10841  seq3fveq2  10914  seqfveq2g  10916  seq3shft2  10920  seqshft2g  10921  seq3split  10927  seqsplitg  10928  seq3caopr3  10930  seqcaopr3g  10931  seqf1oglem2a  10957  seq3id2  10965  seq3homo  10966  seqhomog  10969  m1expcl2  11000  expadd  11020  expmul  11023  faclbnd  11181  hashfzp1  11267  hashmap  11270  hashfacen  11286  hashf1lem2  11288  hashf1  11289  seq3coll  11296  wrdsymb0  11339  len0nnbi  11341  wrd2ind  11497  pfxccatin12lem2c  11504  pfxccatin12lem2  11505  swrdccatin1d  11517  caucvgrelemcau  11748  recan  11877  rexanre  11988  fsumiun  12246  efexp  12451  dvdstr  12597  alzdvds  12623  zob  12660  bitsinv1  12731  gcdmultiplez  12800  dvdssq  12810  cncongr2  12884  prmdiveq  13016  pythagtriplem2  13047  pcexp  13090  elrestr  13603  ptex  13620  xpsff1o  13672  dfgrp3me  13907  mulgneg2  13961  mulgnnass  13962  mhmmulg  13968  rngpropd  14256  ringadd2  14334  mulgass2  14365  opprrngbg  14385  opprsubrngg  14521  subrngpropd  14526  subrgpropd  14563  rhmpropd  14564  lmodprop2d  14687  cnfldmulg  14915  cnfldexp  14916  assapropd  15016  restopn2  15286  txcn  15378  txlm  15382  isxms2  15555  rpcxpmul2  16021  gausslemma2dlem0i  16188  incistruhgr  16343  upgredg2vtx  16401  upgredgpr  16402  uhgr2edg  16459  wlkres  16632  clwwlknonex2  16692  eupth2lem3lem6fi  16724  bj-om  16975  bj-inf2vnlem2  17009  bj-inf2vn  17012  bj-inf2vn2  17013