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  7736  ordpipqqs  7742  mulcmpblnq0  7812  genpprecll  7882  genppreclu  7883  addcmpblnr  8107  ax1rid  8245  axpre-mulgt0  8255  cnegexlem1  8503  msqge0  8947  mulge0  8950  ltleap  8963  nnmulcl  9328  nnsub  9346  elnn0z  9662  ztri3or0  9691  nneoor  9753  uz11  9955  xltnegi  10248  frec2uzuzd  10853  seq3fveq2  10926  seqfveq2g  10928  seq3shft2  10932  seqshft2g  10933  seq3split  10939  seqsplitg  10940  seq3caopr3  10942  seqcaopr3g  10943  seqf1oglem2a  10969  seq3id2  10977  seq3homo  10978  seqhomog  10981  m1expcl2  11012  expadd  11032  expmul  11035  faclbnd  11194  hashfzp1  11280  hashmap  11283  hashfacen  11299  hashf1lem2  11301  hashf1  11302  seq3coll  11309  wrdsymb0  11352  len0nnbi  11354  wrd2ind  11510  pfxccatin12lem2c  11517  pfxccatin12lem2  11518  swrdccatin1d  11530  caucvgrelemcau  11761  recan  11891  rexanre  12002  fsumiun  12262  efexp  12467  dvdstr  12613  alzdvds  12639  zob  12676  bitsinv1  12747  gcdmultiplez  12816  dvdssq  12826  cncongr2  12900  prmdiveq  13036  pythagtriplem2  13067  pcexp  13110  elrestr  13652  ptex  13669  xpsff1o  13721  dfgrp3me  13956  mulgneg2  14010  mulgnnass  14011  mhmmulg  14017  rngpropd  14305  ringadd2  14383  mulgass2  14414  opprrngbg  14434  opprsubrngg  14570  subrngpropd  14575  subrgpropd  14612  rhmpropd  14613  lmodprop2d  14736  cnfldmulg  14964  cnfldexp  14965  assapropd  15065  restopn2  15336  txcn  15428  txlm  15432  isxms2  15605  rpcxpmul2  16071  chtqub  16218  gausslemma2dlem0i  16298  incistruhgr  16453  upgredg2vtx  16511  upgredgpr  16512  uhgr2edg  16569  wlkres  16742  clwwlknonex2  16802  eupth2lem3lem6fi  16834  bj-om  17085  bj-inf2vnlem2  17119  bj-inf2vn  17122  bj-inf2vn2  17123